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

git.iko.soy/Idris-dev

abstract set-prompt into isetPrompt -- and use it

commit50086ac74d7d3699e098b20fadf492d5e5c4776f authorHannes Mehnert <hannes@mehnert.org> dateWed 15 May 2013, 21:39 (13 years ago) parentd7c8e63

3 files changed+10−4

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+5 src/Idris/Prover.hs+3−2 src/Idris/REPL.hs+2−2

src/Idris/AbsSyntax.hs+5

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

286286 RawOutput -> liftIO $ putStrLn s

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

288288

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+

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

290295iWarn fc err = do i <- getIState

291296 case idris_outputmode i of

src/Idris/Prover.hs+3−2

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

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

139139 h' <- getHistory

140140 return (l, Just h')

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

142− return (Just "trivial", h)

141+ IdeSlave n -> -- waitforinput

142+ do isetPrompt prompt

143+ return (Just "trivial", h)

143144 (cmd, step) <- case x of

144145 Nothing -> fail "Abandoned"

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

src/Idris/REPL.hs+2−2

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

9191 = do i <- getIState

9292 case idris_outputmode i of

9393 IdeSlave n ->

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

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

9595 ideslave orig mods

9696

9797

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

122122 idris_outputmode = (IdeSlave id) })

123123 loadModule filename

124124 iucheck

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

125+ isetPrompt (mkPrompt [filename])

126126 -- report success! or failure!

127127 ideslave orig [filename]

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