50086ac · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+5

compare with master

unifiedsplit

@@ -286,6 +286,11 @@ iputGoal s = do i <- getIState

286 RawOutput -> liftIO $ putStrLn s

287 IdeSlave n -> liftIO $ putStrLn $ convSExp "write-goal" s n

288

289+isetPrompt :: String -> Idris ()

290+isetPrompt p = do i <- getIState

291+ case idris_outputmode i of

292+ IdeSlave n -> liftIO $ putStrLn $ convSExp "set-prompt" p n

293+

289iWarn :: FC -> String -> Idris ()

294iWarn :: FC -> String -> Idris ()

290iWarn fc err = do i <- getIState

295iWarn fc err = do i <- getIState

291 case idris_outputmode i of

296 case idris_outputmode i of

src/Idris/Prover.hs+3−2

@@ -138,8 +138,9 @@ ploop d prompt prf e h

138 l <- getInputLine (prompt ++ "> ")

139 h' <- getHistory

140 return (l, Just h')

141− IdeSlave n -> -- setprompt -- waitforinput

141+ IdeSlave n -> -- waitforinput

142+ do isetPrompt prompt

142− return (Just "trivial", h)

143+ return (Just "trivial", h)

143 (cmd, step) <- case x of

144 (cmd, step) <- case x of

144 Nothing -> fail "Abandoned"

145 Nothing -> fail "Abandoned"

145 Just input -> do return (parseTac i input, input)

146 Just input -> do return (parseTac i input, input)

src/Idris/REPL.hs+2−2

@@ -91,7 +91,7 @@ ideslaveStart orig mods

91 = do i <- getIState

92 case idris_outputmode i of

93 IdeSlave n ->

94− when (mods /= []) (do liftIO $ putStrLn $ convSExp "set-prompt" (mkPrompt mods) n)

94+ when (mods /= []) (do isetPrompt (mkPrompt mods))

95 ideslave orig mods

96

97

@@ -122,7 +122,7 @@ ideslave orig mods

122 idris_outputmode = (IdeSlave id) })

123 loadModule filename

124 iucheck

125− liftIO $ putStrLn $ convSExp "set-prompt" (mkPrompt [filename]) id

125+ isetPrompt (mkPrompt [filename])

126 -- report success! or failure!

127 ideslave orig [filename]

128 Nothing -> do iFail "did not understand")