ab67612 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #672 from hannesm/fix-668

ab67612Edwin Brady13 years ago

src/Idris/Help.hs+3−1

compare with master

unifiedsplit

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

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

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

62 , ([":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")

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

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

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

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

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

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

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

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

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

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

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

70 , ([":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)

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

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

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

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

278

279

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

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

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

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

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

301 iPrintResult ""

302 iPrintResult ""

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

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

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

304ideslaveProcess 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)

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

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

305

312

306

313