edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-11-24 04:43:25 +03:00
Code Issues Projects Releases Wiki Activity

Move :exec to the command table

Browse Source
This commit is contained in:
Marshall Bowers 2020-03-26 22:35:27 -04:00
parent 9701a178b5
commit 0371d5b0d1
1 changed files with 1 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/Idris/Parser.idr
View File

@ -1556,6 +1556,7 @@ exprArgCmd names command doc = (names, ExprArg, doc, parse)
parserCommandsForHelp : CommandTable
parserCommandsForHelp =
[ exprArgCmd ["t", "type"] Check "Check the type of an expression"
, exprArgCmd ["exec"] Exec "Compile to an executable and run"
, nameArgCmd ["printdef"] PrintDef "Show the definition of a function"
, nameArgCmd ["s", "search"] ProofSearch "???"
, nameArgCmd ["di"] DebugInfo "???"
@ -1591,9 +1592,6 @@ undocumentedNonEmptyCommand
n <- unqualifiedName
tm <- expr pdef "(interactive)" init
pure (Compile tm n)
<|> do symbol ":"; exactIdent "exec"
tm <- expr pdef "(interactive)" init
pure (Exec tm)
<|> do symbol ":"; replCmd ["log", "logging"]
i <- intLit
pure (SetLog (fromInteger i))