git.iko.soy/Idris-dev
on master help sign in
IDE support for :printdef
fe8927cDavid Raymond Christiansen
src/Idris/IdeSlave.hs+2
compare with master
unifiedsplit
@@ -218,6 +218,7 @@ data IdeSlaveCommand = REPLCompletions String
218 | TermNormalise [(Name, Bool)] Term
218 | TermNormalise [(Name, Bool)] Term
219 | TermShowImplicits [(Name, Bool)] Term
219 | TermShowImplicits [(Name, Bool)] Term
220 | TermNoImplicits [(Name, Bool)] Term
220 | TermNoImplicits [(Name, Bool)] Term
221+ | PrintDef String
221
222
222sexpToCommand :: SExp -> Maybe IdeSlaveCommand
223sexpToCommand :: SExp -> Maybe IdeSlaveCommand
223sexpToCommand (SexpList (x:[])) = sexpToCommand x
224sexpToCommand (SexpList (x:[])) = sexpToCommand x
@@ -260,6 +261,7 @@ sexpToCommand (SexpList [SymbolAtom "show-term-implicits", StringAtom encoded])
260 Just (TermShowImplicits bnd tm)
261 Just (TermShowImplicits bnd tm)
261sexpToCommand (SexpList [SymbolAtom "hide-term-implicits", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in
262sexpToCommand (SexpList [SymbolAtom "hide-term-implicits", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in
262 Just (TermNoImplicits bnd tm)
263 Just (TermNoImplicits bnd tm)
264+sexpToCommand (SexpList [SymbolAtom "print-definition", StringAtom name]) = Just (PrintDef name)
263sexpToCommand _ = Nothing
265sexpToCommand _ = Nothing
264
266
265parseMessage :: String -> Either Err (SExp, Integer)
267parseMessage :: String -> Either Err (SExp, Integer)
src/Idris/REPL.hs+10
@@ -477,6 +477,16 @@ runIdeSlaveCommand h id orig fn modes (IdeSlave.TermShowImplicits bnd tm) =
477 ideSlaveForceTermImplicits h id bnd True tm
477 ideSlaveForceTermImplicits h id bnd True tm
478runIdeSlaveCommand h id orig fn modes (IdeSlave.TermNoImplicits bnd tm) =
478runIdeSlaveCommand h id orig fn modes (IdeSlave.TermNoImplicits bnd tm) =
479 ideSlaveForceTermImplicits h id bnd False tm
479 ideSlaveForceTermImplicits h id bnd False tm
480+runIdeSlaveCommand h id orig fn mods (IdeSlave.PrintDef name) =
481+ case splitName name of
482+ Left err -> iPrintError err
483+ Right n -> process "(ideslave)" (PrintDef n)
484+ where splitName :: String -> Either String Name
485+ splitName s = case reverse $ splitOn "." s of
486+ [] -> Left ("Didn't understand name '" ++ s ++ "'")
487+ [n] -> Right $ sUN n
488+ (n:ns) -> Right $ sNS (sUN n) ns
489+
480
490
481-- | Show a term for IDESlave with the specified implicitness
491-- | Show a term for IDESlave with the specified implicitness
482ideSlaveForceTermImplicits :: Handle -> Integer -> [(Name, Bool)] -> Bool -> Term -> Idris ()
492ideSlaveForceTermImplicits :: Handle -> Integer -> [(Name, Bool)] -> Bool -> Term -> Idris ()