b8a2bbf · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+1

@@ -116,6 +116,7 @@ data Command = Quit | Help | Eval PTerm

116 | Compile String

117 | Metavars

118 | TTShell

119+ | LogLvl Int

119 | NOP

120 | NOP

120

121

121-- Parsed declarations

122-- Parsed declarations

src/Idris/REPL.hs+1

@@ -55,6 +55,7 @@ process TTShell = do ist <- get

55 shst' <- lift $ runShell shst

56 return ()

57process (Compile f) = do compile f

58+process (LogLvl i) = setLogLevel i

58process Metavars = do ist <- get

59process Metavars = do ist <- get

59 let mvs = idris_metavars ist \\ primDefs

60 let mvs = idris_metavars ist \\ primDefs

60 case mvs of

61 case mvs of

src/Idris/REPLParser.hs+1

@@ -24,5 +24,6 @@ pCmd = try (do cmd ["q", "quit"]; return Quit)

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

25 <|> try (do cmd ["c", "compile"]; f <- identifier; return (Compile f))

26 <|> try (do cmd ["m", "metavars"]; return Metavars)

27+ <|> try (do cmd ["log"]; i <- natural; return (LogLvl (fromIntegral i)))

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

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

28 <|> do eof; return NOP

29 <|> do eof; return NOP