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

git.iko.soy/Idris-dev

add command to change current directory

commit75e01411a2192d893319491c75f7c79ba9da6ccf authorHannes Mehnert <hannes@mehnert.org> dateSat 23 Mar 2013, 12:48 (14 years ago) parent7308d26

4 files changed+6

unifiedsplit

src/Idris/AbsSyntaxTree.hs+1

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

167167 | TotCheck Name

168168 | Reload

169169 | Load FilePath

170+ | ChangeDirectory FilePath

170171 | ModImport String

171172 | Edit

172173 | Compile Target String

src/Idris/Help.hs+1

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

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

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

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

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

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

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

3334 ([":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

179179

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

181181process fn Help = iputStrLn displayHelp

182+process fn (ChangeDirectory f)

183+ = do liftIO $ setCurrentDirectory f

184+ return ()

182185process fn (Eval t)

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

184187 ctxt <- getContext

src/Idris/REPLParser.hs+1

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

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

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

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

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

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

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

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