@@ -216,94 +216,112 @@ ideslave orig mods
216216 (f:_) -> f
217217 _ -> ""
218218 case IdeSlave.sexpToCommand sexp of
219− Just (IdeSlave.Interpret cmd) ->
220− do c <- colourise
221− case parseCmd i "(input)" cmd of
222− Failure err -> iPrintError $ show (fixColour c err)
223− Success (Prove n') -> do iPrintResult ""
224− idrisCatch
225− (process stdout fn (Prove n'))
226− (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)
227− isetPrompt (mkPrompt mods)
228− Success cmd -> idrisCatch
229− (ideslaveProcess fn cmd)
230− (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)
231− Just (IdeSlave.REPLCompletions str) ->
232− do (unused, compls) <- replCompletion (reverse str, "")
233− let good = IdeSlave.SexpList [IdeSlave.SymbolAtom "ok", IdeSlave.toSExp (map replacement compls, reverse unused)]
234− runIO $ putStrLn $ IdeSlave.convSExp "return" good id
235− Just (IdeSlave.LoadFile filename) ->
236− do clearErr
237− putIState (orig { idris_options = idris_options i,
238− idris_outputmode = (IdeSlave id) })
239− loadInputs stdout [filename]
240− isetPrompt (mkPrompt [filename])
241− -- Report either success or failure
242− i <- getIState
243− case (errSpan i) of
244− Nothing -> iPrintResult $ "loaded " ++ filename
245− Just x -> iPrintError $ "didn't load " ++ filename
246− ideslave orig [filename]
247− Just (IdeSlave.TypeOf name) ->
248− case splitName name of
249− Left err -> iPrintError err
250− Right n -> process stdout "(ideslave)"
251− (Check (PRef (FC "(ideslave)" (0,0) (0,0)) n))
252− Just (IdeSlave.DocsFor name) ->
253− case splitName name of
254− Left err -> iPrintError err
255− Right n -> process stdout "(ideslave)" (DocStr n)
256− Just (IdeSlave.CaseSplit line name) ->
257− process stdout fn (CaseSplitAt False line (sUN name))
258− Just (IdeSlave.AddClause line name) ->
259− process stdout fn (AddClauseFrom False line (sUN name))
260− Just (IdeSlave.AddProofClause line name) ->
261− process stdout fn (AddProofClauseFrom False line (sUN name))
262− Just (IdeSlave.AddMissing line name) ->
263− process stdout fn (AddMissing False line (sUN name))
264− Just (IdeSlave.MakeWithBlock line name) ->
265− process stdout fn (MakeWith False line (sUN name))
266− Just (IdeSlave.ProofSearch line name hints) ->
267− process stdout fn (DoProofSearch False line (sUN name) (map sUN hints))
268− Just (IdeSlave.Apropos a) ->
269− process stdout fn (Apropos a)
270− Just (IdeSlave.GetOpts) ->
271− do ist <- getIState
272− let opts = idris_options ist
273− let impshow = opt_showimp opts
274− let errCtxt = opt_errContext opts
275− let options = (IdeSlave.SymbolAtom "ok",
276− [(IdeSlave.SymbolAtom "show-implicits", impshow),
277− (IdeSlave.SymbolAtom "error-context", errCtxt)])
278− runIO . putStrLn $ IdeSlave.convSExp "return" options id
279− Just (IdeSlave.SetOpt IdeSlave.ShowImpl b) ->
280− do setImpShow b
281− let msg = (IdeSlave.SymbolAtom "ok", b)
282− runIO . putStrLn $ IdeSlave.convSExp "return" msg id
283− Just (IdeSlave.SetOpt IdeSlave.ErrContext b) ->
284− do setErrContext b
285− let msg = (IdeSlave.SymbolAtom "ok", b)
286− runIO . putStrLn $ IdeSlave.convSExp "return" msg id
287− Just (IdeSlave.Metavariables cols) ->
288− do ist <- getIState
289− let mvs = reverse $ map fst (idris_metavars ist) \\ primDefs
290− imp <- impShow
291− let mvarTys = map (delabTy ist) mvs
292− let res = (IdeSlave.SymbolAtom "ok",
293− zipWith (\ n (prems, concl) -> (n, prems, concl))
294− (map (IdeSlave.StringAtom . show) mvs)
295− (map (sexpGoal ist cols imp [] . getGoal) mvarTys))
296− runIO . putStrLn $ IdeSlave.convSExp "return" res id
297− Nothing -> do iPrintError "did not understand")
219+ Just cmd -> runIdeSlaveCommand id orig fn mods cmd
220+ Nothing -> iPrintError "did not understand" )
298221 (\e -> do iPrintError $ show e))
299222 (\e -> do iPrintError $ show e)
300223 ideslave orig mods
224+
225+-- | Run IDESlave commands
226+runIdeSlaveCommand :: Integer -- ^^ The continuation ID for the client
227+ -> IState -- ^^ The original IState
228+ -> FilePath -- ^^ The current open file
229+ -> [FilePath] -- ^^ The currently loaded modules
230+ -> IdeSlave.IdeSlaveCommand -- ^^ The command to process
231+ -> Idris ()
232+runIdeSlaveCommand id orig fn mods (IdeSlave.Interpret cmd) =
233+ do c <- colourise
234+ i <- getIState
235+ case parseCmd i "(input)" cmd of
236+ Failure err -> iPrintError $ show (fixColour c err)
237+ Success (Prove n') -> do iPrintResult ""
238+ idrisCatch
239+ (process stdout fn (Prove n'))
240+ (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)
241+ isetPrompt (mkPrompt mods)
242+ Success cmd -> idrisCatch
243+ (ideslaveProcess fn cmd)
244+ (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)
245+runIdeSlaveCommand id orig fn mods (IdeSlave.REPLCompletions str) =
246+ do (unused, compls) <- replCompletion (reverse str, "")
247+ let good = IdeSlave.SexpList [IdeSlave.SymbolAtom "ok",
248+ IdeSlave.toSExp (map replacement compls,
249+ reverse unused)]
250+ runIO $ putStrLn $ IdeSlave.convSExp "return" good id
251+runIdeSlaveCommand id orig fn mods (IdeSlave.LoadFile filename) =
252+ do i <- getIState
253+ clearErr
254+ putIState (orig { idris_options = idris_options i,
255+ idris_outputmode = (IdeSlave id) })
256+ loadInputs stdout [filename]
257+ isetPrompt (mkPrompt [filename])
258+ -- Report either success or failure
259+ i <- getIState
260+ case (errSpan i) of
261+ Nothing -> iPrintResult $ "loaded " ++ filename
262+ Just x -> iPrintError $ "didn't load " ++ filename
263+ ideslave orig [filename]
264+runIdeSlaveCommand id orig fn mods (IdeSlave.TypeOf name) =
265+ case splitName name of
266+ Left err -> iPrintError err
267+ Right n -> process stdout "(ideslave)"
268+ (Check (PRef (FC "(ideslave)" (0,0) (0,0)) n))
269+ where splitName :: String -> Either String Name
270+ splitName s = case reverse $ splitOn "." s of
271+ [] -> Left ("Didn't understand name '" ++ s ++ "'")
272+ [n] -> Right $ sUN n
273+ (n:ns) -> Right $ sNS (sUN n) ns
274+runIdeSlaveCommand id orig fn mods (IdeSlave.DocsFor name) =
275+ case splitName name of
276+ Left err -> iPrintError err
277+ Right n -> process stdout "(ideslave)" (DocStr n)
301278 where splitName :: String -> Either String Name
302279 splitName s = case reverse $ splitOn "." s of
303280 [] -> Left ("Didn't understand name '" ++ s ++ "'")
304281 [n] -> Right $ sUN n
305282 (n:ns) -> Right $ sNS (sUN n) ns
306− getGoal :: PTerm -> ([(Name, PTerm)], PTerm)
283+runIdeSlaveCommand id orig fn mods (IdeSlave.CaseSplit line name) =
284+ process stdout fn (CaseSplitAt False line (sUN name))
285+runIdeSlaveCommand id orig fn mods (IdeSlave.AddClause line name) =
286+ process stdout fn (AddClauseFrom False line (sUN name))
287+runIdeSlaveCommand id orig fn mods (IdeSlave.AddProofClause line name) =
288+ process stdout fn (AddProofClauseFrom False line (sUN name))
289+runIdeSlaveCommand id orig fn mods (IdeSlave.AddMissing line name) =
290+ process stdout fn (AddMissing False line (sUN name))
291+runIdeSlaveCommand id orig fn mods (IdeSlave.MakeWithBlock line name) =
292+ process stdout fn (MakeWith False line (sUN name))
293+runIdeSlaveCommand id orig fn mods (IdeSlave.ProofSearch line name hints) =
294+ process stdout fn (DoProofSearch False line (sUN name) (map sUN hints))
295+runIdeSlaveCommand id orig fn mods (IdeSlave.Apropos a) =
296+ process stdout fn (Apropos a)
297+runIdeSlaveCommand id orig fn mods (IdeSlave.GetOpts) =
298+ do ist <- getIState
299+ let opts = idris_options ist
300+ let impshow = opt_showimp opts
301+ let errCtxt = opt_errContext opts
302+ let options = (IdeSlave.SymbolAtom "ok",
303+ [(IdeSlave.SymbolAtom "show-implicits", impshow),
304+ (IdeSlave.SymbolAtom "error-context", errCtxt)])
305+ runIO . putStrLn $ IdeSlave.convSExp "return" options id
306+runIdeSlaveCommand id orig fn mods (IdeSlave.SetOpt IdeSlave.ShowImpl b) =
307+ do setImpShow b
308+ let msg = (IdeSlave.SymbolAtom "ok", b)
309+ runIO . putStrLn $ IdeSlave.convSExp "return" msg id
310+runIdeSlaveCommand id orig fn mods (IdeSlave.SetOpt IdeSlave.ErrContext b) =
311+ do setErrContext b
312+ let msg = (IdeSlave.SymbolAtom "ok", b)
313+ runIO . putStrLn $ IdeSlave.convSExp "return" msg id
314+runIdeSlaveCommand id orig fn mods (IdeSlave.Metavariables cols) =
315+ do ist <- getIState
316+ let mvs = reverse $ map fst (idris_metavars ist) \\ primDefs
317+ imp <- impShow
318+ let mvarTys = map (delabTy ist) mvs
319+ let res = (IdeSlave.SymbolAtom "ok",
320+ zipWith (\ n (prems, concl) -> (n, prems, concl))
321+ (map (IdeSlave.StringAtom . show) mvs)
322+ (map (sexpGoal ist cols imp [] . getGoal) mvarTys))
323+ runIO . putStrLn $ IdeSlave.convSExp "return" res id
324+ where getGoal :: PTerm -> ([(Name, PTerm)], PTerm)
307325 getGoal (PPi _ n t sc) = let (prems, conc) = getGoal sc
308326 in ((n, t):prems, conc)
309327 getGoal tm = ([], tm)
@@ -325,6 +343,7 @@ ideslave orig mods
325343 rest = sexpGoal ist cols imp (n:ns) (ps, concl)
326344 in ((n', t', spans) : fst rest, snd rest)
327345
346+
328347ideslaveProcess :: FilePath -> Command -> Idris ()
329348ideslaveProcess fn Help = process stdout fn Help
330349ideslaveProcess fn (ChangeDirectory f) = do process stdout fn (ChangeDirectory f)