edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-11-27 18:53:42 +03:00
Code Issues Projects Releases Wiki Activity

Reorder commands to the way they were prior to changes

Browse Source
This commit is contained in:
Marshall Bowers 2020-03-27 23:29:54 -04:00
parent 476e776083
commit a5fa2e00e6
1 changed files with 5 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
src/Idris/Parser.idr
View File

@ -1576,19 +1576,19 @@ exprArgCmd parseCmd command doc = (names, ExprArg, doc, parse)
parserCommandsForHelp : CommandTable
parserCommandsForHelp =
[ exprArgCmd (ParseREPLCmd ["t", "type"]) Check "Check the type of an expression"
, exprArgCmd (ParseIdentCmd "exec") Exec "Compile to an executable and run"
, nameArgCmd (ParseREPLCmd ["printdef"]) PrintDef "Show the definition of a function"
, nameArgCmd (ParseREPLCmd ["s", "search"]) ProofSearch "???"
, nameArgCmd (ParseIdentCmd "di") DebugInfo "???"
, nameArgCmd (ParseREPLCmd ["miss", "missing"]) Missing "Show missing clauses"
, nameArgCmd (ParseKeywordCmd "total") Total "Check the totality of a name"
, noArgCmd (ParseREPLCmd ["h", "help"]) Help "Display this help text"
, noArgCmd (ParseREPLCmd ["q", "quit", "exit"]) Quit "Exit the Idris system"
, noArgCmd (ParseREPLCmd ["cwd"]) CWD "Displays the current working directory"
, noArgCmd (ParseREPLCmd ["version"]) ShowVersion "Display the Idris version"
, exprArgCmd (ParseIdentCmd "exec") Exec "Compile to an executable and run"
, noArgCmd (ParseREPLCmd ["r", "reload"]) Reload "Reload current file"
, noArgCmd (ParseREPLCmd ["e", "edit"]) Edit "Edit current file using $EDITOR or $VISUAL"
, nameArgCmd (ParseREPLCmd ["miss", "missing"]) Missing "Show missing clauses"
, nameArgCmd (ParseKeywordCmd "total") Total "Check the totality of a name"
, noArgCmd (ParseREPLCmd ["m", "metavars"]) Metavars "Show remaining proof obligations (metavariables or holes)"
, noArgCmd (ParseREPLCmd ["version"]) ShowVersion "Display the Idris version"
, noArgCmd (ParseREPLCmd ["h", "help"]) Help "Display this help text"
]
export