5075b24 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Support for the new interactive commands via the IdeSlave REPL

Also, add ":addmissing" and ":addmissing!" to completions of the REPL fixes #668

commit5075b246b54ff6f4eaac6ea851b313502b0d813c authorHannes Mehnert <hannes@mehnert.org> dateTue 26 Nov 2013, 18:10 (13 years ago) parent77b1faf

2 files changed+10−1

unifiedsplit

src/Idris/Help.hs+3−1

@@ -60,10 +60,12 @@ extraHelp =

6060 , ([":casesplit!", ":cs!"], NoArg, ":cs! <line> <name> destructively splits the pattern variable on the line")

6161 , ([":addclause", ":ac"], NoArg, ":ac <line> <name> adds a clause for the definition of the name on the line")

6262 , ([":addclause!", ":ac!"], NoArg, ":ac! <line> <name> destructively adds a clause for the definition of the name on the line")

63+ , ([":addmissing", ":am"], NoArg, ":am <line> <name> adds all missing pattern matches for the name on the line")

64+ , ([":addmissing!", ":am!"], NoArg, ":am! <line> <name> destructively adds all missing pattern matches for the name on the line")

6365 , ([":makewith", ":mw"], NoArg, ":mw <line> <name> adds a with clause for the definition of the name on the line")

6466 , ([":makewith!", ":mw!"], NoArg, ":mw! <line> <name> destructively adds a with clause for the definition of the name on the line")

6567 , ([":proofsearch", ":ps"], NoArg, ":ps <line> <name> <names> does proof search for name on line, with names as hints")

6668 , ([":proofsearch!", ":ps!"], NoArg, ":ps! <line> <name> <names> destructively does proof search for name on line, with names as hints")

6769 , ([":addproofclause", ":apc"], NoArg, ":apc <line> <name> adds a pattern-matching proof clause to name on line")

6870 , ([":addproofclause!", ":apc!"], NoArg, ":apc! <line> <name> destructively adds a pattern-matching proof clause to name on line")

69− ]

71+ ]

src/Idris/REPL.hs+7

@@ -275,6 +275,7 @@ ideslaveProcess fn (Spec t) = process stdout fn (Spec t)

275275ideslaveProcess fn (ShowProof n') = process stdout fn (ShowProof n')

276276ideslaveProcess fn (HNF t) = process stdout fn (HNF t)

277277--ideslaveProcess fn TTShell = process stdout fn TTShell -- need some prove mode!

278+ideslaveProcess fn (TestInline t) = process stdout fn (TestInline t)

278279

279280--that most likely does not work, since we need to wrap

280281--input/output of the executed binary...

@@ -301,6 +302,12 @@ ideslaveProcess fn (UnsetOpt ShowImpl) = do process stdout fn (UnsetOpt ShowImpl

301302 iPrintResult ""

302303ideslaveProcess fn (SetOpt x) = process stdout fn (SetOpt x)

303304ideslaveProcess fn (UnsetOpt x) = process stdout fn (UnsetOpt x)

305+ideslaveProcess fn (CaseSplitAt False pos str) = process stdout fn (CaseSplitAt False pos str)

306+ideslaveProcess fn (AddProofClauseFrom False pos str) = process stdout fn (AddProofClauseFrom False pos str)

307+ideslaveProcess fn (AddClauseFrom False pos str) = process stdout fn (AddClauseFrom False pos str)

308+ideslaveProcess fn (AddMissing False pos str) = process stdout fn (AddMissing False pos str)

309+ideslaveProcess fn (MakeWith False pos str) = process stdout fn (MakeWith False pos str)

310+ideslaveProcess fn (DoProofSearch False pos str xs) = process stdout fn (DoProofSearch False pos str xs)

304311ideslaveProcess fn _ = iPrintError "command not recognized or not supported"

305312

306313