6fb995d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

support for add-proof-clause in IdeSlave

commit6fb995d27ad2eb4d8403dd2e3fbef7f438f592e4 authorHannes Mehnert <hannes@mehnert.org> dateTue 19 Nov 2013, 00:16 (13 years ago) parentf6edbf0

2 files changed+4

compare with master

unifiedsplit

src/Idris/IdeSlave.hs+2 src/Idris/REPL.hs+2

src/Idris/IdeSlave.hs+2

@@ -97,6 +97,7 @@ data IdeSlaveCommand = REPLCompletions String

9797 | TypeOf String

9898 | CaseSplit Int String

9999 | AddClause Int String

100+ | AddProofClause Int String

100101 | AddMissing Int String

101102 | MakeWithBlock Int String

102103 | ProofSearch Int String [String]

@@ -111,6 +112,7 @@ sexpToCommand (SexpList [SymbolAtom "load-file", StringAtom filename])

111112sexpToCommand (SexpList [SymbolAtom "type-of", StringAtom name]) = Just (TypeOf name)

112113sexpToCommand (SexpList [SymbolAtom "case-split", IntegerAtom line, StringAtom name]) = Just (CaseSplit (fromInteger line) name)

113114sexpToCommand (SexpList [SymbolAtom "add-clause", IntegerAtom line, StringAtom name]) = Just (AddClause (fromInteger line) name)

115+sexpToCommand (SexpList [SymbolAtom "add-proof-clause", IntegerAtom line, StringAtom name]) = Just (AddProofClause (fromInteger line) name)

114116sexpToCommand (SexpList [SymbolAtom "add-missing", IntegerAtom line, StringAtom name]) = Just (AddMissing (fromInteger line) name)

115117sexpToCommand (SexpList [SymbolAtom "make-with", IntegerAtom line, StringAtom name]) = Just (MakeWithBlock (fromInteger line) name)

116118sexpToCommand (SexpList [SymbolAtom "proof-search", IntegerAtom line, StringAtom name, SexpList hintexp]) | Just hints <- getHints hintexp = Just (ProofSearch (fromInteger line) name hints)

src/Idris/REPL.hs+2

@@ -239,6 +239,8 @@ ideslave orig mods

239239 process stdout fn (CaseSplitAt False line (UN name))

240240 Just (IdeSlave.AddClause line name) ->

241241 process stdout fn (AddClauseFrom False line (UN name))

242+ Just (IdeSlave.AddProofClause line name) ->

243+ process stdout fn (AddProofClauseFrom False line (UN name))

242244 Just (IdeSlave.AddMissing line name) ->

243245 process stdout fn (AddMissing False line (UN name))

244246 Just (IdeSlave.MakeWithBlock line name) ->