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

git.iko.soy/Idris-dev

on master help sign in

support for add-proof-clause in IdeSlave

6fb995dHannes Mehnert13 years ago

src/Idris/IdeSlave.hs+2

compare with master

unifiedsplit

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

97 | TypeOf String

98 | CaseSplit Int String

99 | AddClause Int String

100+ | AddProofClause Int String

100 | AddMissing Int String

101 | AddMissing Int String

101 | MakeWithBlock Int String

102 | MakeWithBlock Int String

102 | ProofSearch Int String [String]

103 | ProofSearch Int String [String]

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

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

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

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

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

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

114sexpToCommand (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)

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

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

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

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

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

118sexpToCommand (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

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

240 Just (IdeSlave.AddClause line name) ->

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

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

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

242 Just (IdeSlave.AddMissing line name) ->

244 Just (IdeSlave.AddMissing line name) ->

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

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

244 Just (IdeSlave.MakeWithBlock line name) ->

246 Just (IdeSlave.MakeWithBlock line name) ->