f85d1f0 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

:ttshell

commitf85d1f0f55b74e7b063546be8870faaae38d8474 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateThu 6 Oct 2011, 23:53 (15 years ago) parenta8768af

4 files changed+9−2

compare with master

unifiedsplit

src/Core/ProofShell.hs+2−2 src/Idris/AbsSyntax.hs+1 src/Idris/REPL.hs+5 src/Idris/REPLParser.hs+1

src/Core/ProofShell.hs+2−2

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

5555

5656runShell :: ShellState -> IO ShellState

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

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

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

5959 (\st -> do print st

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

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

6161 (prf st)

6262 x <- readline prompt

6363 cmd <- case x of

src/Idris/AbsSyntax.hs+1

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

4747-- Commands in the REPL

4848

4949data Command = Quit | Help | Eval PTerm

50+ | TTShell

5051 | NOP

5152

5253-- Parsed declarations

src/Idris/REPL.hs+5

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

55import Idris.AbsSyntax

66import Idris.REPLParser

7+import Core.ProofShell

89import System.Console.Readline

910import Control.Monad

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

3334process Help

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

3536process (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 ()

3641process NOP = return ()

3742

src/Idris/REPLParser.hs+1

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

2121pCmd :: IParser Command

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

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

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

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

2526 <|> do eof; return NOP