f85d1f0 · Idris-dev · git.iko.soy

src/Core/ProofShell.hs+2−2

compare with master

unifiedsplit

@@ -55,9 +55,9 @@ processCommand (Tac e) state

55

56runShell :: ShellState -> IO ShellState

57runShell st = do (prompt, parser) <-

58− maybe (return ("> ", parseCommand))

58+ maybe (return ("TT# ", parseCommand))

59 (\st -> do print st

60− return (show (thname st) ++ "> ", parseTactic))

60+ return (show (thname st) ++ "# ", parseTactic))

61 (prf st)

62 x <- readline prompt

63 cmd <- case x of

src/Idris/AbsSyntax.hs+1

@@ -47,6 +47,7 @@ iLOG str = do i <- get

47-- Commands in the REPL

48

49data Command = Quit | Help | Eval PTerm

50+ | TTShell

50 | NOP

51 | NOP

51

52

52-- Parsed declarations

53-- Parsed declarations

src/Idris/REPL.hs+5

@@ -4,6 +4,7 @@ module Idris.REPL where

4

5import Idris.AbsSyntax

6import Idris.REPLParser

7+import Core.ProofShell

7

8

8import System.Console.Readline

9import System.Console.Readline

9import Control.Monad

10import Control.Monad

@@ -33,5 +34,9 @@ process :: Command -> Idris ()

33process Help

34process Help

34 = iputStrLn "At some point I'll write some help text. Thanks for asking though."

35 = iputStrLn "At some point I'll write some help text. Thanks for asking though."

35process (Eval t) = iputStrLn $ "Not implemented: " ++ show t

36process (Eval t) = iputStrLn $ "Not implemented: " ++ show t

37+process TTShell = do ist <- get

38+ let shst = initState (tt_ctxt ist)

39+ shst' <- lift $ runShell shst

40+ return ()

36process NOP = return ()

41process NOP = return ()

37

42

src/Idris/REPLParser.hs+1

@@ -21,5 +21,6 @@ cmd xs = do lchar ':'; docmd xs

21pCmd :: IParser Command

22pCmd = try (do cmd ["q", "quit"]; return Quit)

23 <|> try (do cmd ["h", "?", "help"]; return Help)

24+ <|> try (do cmd ["ttshell"]; return TTShell)

24 <|> do t <- pFullExpr; return (Eval t)

25 <|> do t <- pFullExpr; return (Eval t)

25 <|> do eof; return NOP

26 <|> do eof; return NOP