dbe880c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

support for add-clause in IdeSlave

dbe880cHannes Mehnert13 years ago

src/Idris/IdeSlave.hs+2

compare with master

unifiedsplit

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

95 | Interpret String

96 | TypeOf String

97 | CaseSplit Int String

98+ | AddClause Int String

98 | LoadFile String

99 | LoadFile String

99 deriving Show

100 deriving Show

100

101

@@ -105,6 +106,7 @@ sexpToCommand (SexpList [SymbolAtom "repl-completions", StringAtom prefix])

105sexpToCommand (SexpList [SymbolAtom "load-file", StringAtom filename]) = Just (LoadFile filename)

106sexpToCommand (SexpList [SymbolAtom "load-file", StringAtom filename]) = Just (LoadFile filename)

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

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

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

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

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

108sexpToCommand _ = Nothing

110sexpToCommand _ = Nothing

109

111

110parseMessage :: String -> Either Err (SExp, Integer)

112parseMessage :: String -> Either Err (SExp, Integer)

src/Idris/REPL.hs+3−1

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

237 process stdout "(ideslave)" (Check (PRef (FC "(ideslave)" 0 0) (UN name)))

238 Just (IdeSlave.CaseSplit line name) ->

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

240+ Just (IdeSlave.AddClause line name) ->

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

240 Nothing -> do iPrintError "did not understand")

242 Nothing -> do iPrintError "did not understand")

241 (\e -> do iPrintError $ show e)

243 (\e -> do iPrintError $ show e)

242 ideslave orig mods

244 ideslave orig mods

@@ -572,7 +574,7 @@ process h fn (AddClauseFrom updatefile l n)

572 cl ++ "\n" ++

574 cl ++ "\n" ++

573 unlines rest)

575 unlines rest)

574 runIO $ copyFile fb fn

576 runIO $ copyFile fb fn

575− else ihputStrLn h cl

577+ else ihPrintResult h cl

576 where

578 where

577 getIndent i n [] = 0

579 getIndent i n [] = 0

578 getIndent i n xs | take (length n) xs == n = i

580 getIndent i n xs | take (length n) xs == n = i