75e0141 · Idris-dev · git.iko.soy

src/Idris/AbsSyntaxTree.hs+1

compare with master

unifiedsplit

@@ -167,6 +167,7 @@ data Command = Quit

167 | TotCheck Name

168 | Reload

169 | Load FilePath

170+ | ChangeDirectory FilePath

170 | ModImport String

171 | ModImport String

171 | Edit

172 | Edit

172 | Compile Target String

173 | Compile Target String

src/Idris/Help.hs+1

@@ -28,6 +28,7 @@ help =

28 ([":total"], NameArg, "Check the totality of a name"),

29 ([":r",":reload"], NoArg, "Reload current file"),

30 ([":l",":load"], FileArg, "Load a new file"),

31+ ([":cd"], FileArg, "Change working directory"),

31 ([":m",":module"], ModuleArg, "Import an extra module"), -- NOTE: dragons

32 ([":m",":module"], ModuleArg, "Import an extra module"), -- NOTE: dragons

32 ([":e",":edit"], NoArg, "Edit current file using $EDITOR or $VISUAL"),

33 ([":e",":edit"], NoArg, "Edit current file using $EDITOR or $VISUAL"),

33 ([":m",":metavars"], MetaVarArg, "Show remaining proof obligations (metavariables)"),

34 ([":m",":metavars"], MetaVarArg, "Show remaining proof obligations (metavariables)"),

src/Idris/REPL.hs+3

@@ -179,6 +179,9 @@ insertScript prf (x : xs) = x : insertScript prf xs

179

180process :: FilePath -> Command -> Idris ()

181process fn Help = iputStrLn displayHelp

182+process fn (ChangeDirectory f)

183+ = do liftIO $ setCurrentDirectory f

184+ return ()

182process fn (Eval t)

185process fn (Eval t)

183 = do (tm, ty) <- elabVal toplevel False t

186 = do (tm, ty) <- elabVal toplevel False t

184 ctxt <- getContext

187 ctxt <- getContext

src/Idris/REPLParser.hs+1

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

45 <|> try (do cmd ["showproof"]; n <- pName; eof; return (ShowProof n))

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

47 <|> try (do cmd ["l", "load"]; f <- getInput; return (Load f))

48+ <|> try (do cmd ["cd"]; f <- getInput; return (ChangeDirectory f))

48 <|> try (do cmd ["spec"]; t <- pFullExpr defaultSyntax; return (Spec t))

49 <|> try (do cmd ["spec"]; t <- pFullExpr defaultSyntax; return (Spec t))

49 <|> try (do cmd ["hnf"]; t <- pFullExpr defaultSyntax; return (HNF t))

50 <|> try (do cmd ["hnf"]; t <- pFullExpr defaultSyntax; return (HNF t))

50 <|> try (do cmd ["doc"]; n <- pfName; eof; return (DocStr n))

51 <|> try (do cmd ["doc"]; n <- pfName; eof; return (DocStr n))