git.iko.soy/Idris-dev
on master help sign in
Merge pull request #575 from david-christiansen/tab-new-cmds

Add new editor commands to tab completion

commitb095ac018bc9211f73964508fba4a71c6d915730 authorEdwin Brady <edwin.brady@gmail.com> dateFri 1 Nov 2013, 08:04 (13 years ago) parentafef29e91317fb
2 files changed+17−2
compare with master
unifiedsplit
src/Idris/Completion.hs+1−1 src/Idris/Help.hs+16−1
src/Idris/Completion.hs+1−1
@@ -22,7 +22,7 @@ import System.Console.ANSI (Color)
2222fst3 :: (a, b, c) -> a
2323fst3 (a, b, c) = a
2424
25−commands = concatMap fst3 help
25+commands = concatMap fst3 (help ++ extraHelp)
2626
2727-- | A specification of the arguments that tactics can take
2828data TacticArg = NameTArg -- ^ Names: n1, n2, n3, ... n
src/Idris/Help.hs+16−1
@@ -1,4 +1,4 @@
1−module Idris.Help (CmdArg(..), help) where
1+module Idris.Help (CmdArg(..), help, extraHelp) where
22
33data CmdArg = ExprArg -- ^ The command takes an expression
44 | NameArg -- ^ The command takes a name
@@ -51,3 +51,18 @@ help =
5151 ([":colour", ":color"], ColourArg, "Turn REPL colours on or off; set a specific colour"),
5252 ([":q",":quit"], NoArg, "Exit the Idris system")
5353 ]
54+
55+-- | Use these for completion, but don't show them in :help
56+extraHelp ::[([String], CmdArg, String)]
57+extraHelp =
58+ [ ([":casesplit", ":cs"], NoArg, ":cs <line> <name> splits the pattern variable on the line")
59+ , ([":casesplit!", ":cs!"], NoArg, ":cs! <line> <name> destructively splits the pattern variable on the line")
60+ , ([":addclause", ":ac"], NoArg, ":ac <line> <name> adds a clause for the definition of the name on the line")
61+ , ([":addclause!", ":ac!"], NoArg, ":ac! <line> <name> destructively adds a clause for the definition of the name on the line")
62+ , ([":makewith", ":mw"], NoArg, ":mw <line> <name> adds a with clause for the definition of the name on the line")
63+ , ([":makewith!", ":mw!"], NoArg, ":mw! <line> <name> destructively adds a with clause for the definition of the name on the line")
64+ , ([":proofsearch", ":ps"], NoArg, ":ps <line> <name> <names> does proof search for name on line, with names as hints")
65+ , ([":proofsearch!", ":ps!"], NoArg, ":ps! <line> <name> <names> destructively does proof search for name on line, with names as hints")
66+ , ([":addproofclause", ":apc"], NoArg, ":apc <line> <name> adds a pattern-matching proof clause to name on line")
67+ , ([":addproofclause!", ":apc!"], NoArg, ":apc! <line> <name> destructively adds a pattern-matching proof clause to name on line")
68+ ]