git.iko.soy/Idris-dev
on master help sign in
IDE support for :printdef
commitfe8927cae6694f2c37dbc36657780f155bb9b4e5 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateWed 24 Sep 2014, 14:16 (12 years ago) parent6de02da
2 files changed+12
compare with master
unifiedsplit
src/Idris/IdeSlave.hs+2 src/Idris/REPL.hs+10
src/Idris/IdeSlave.hs+2
@@ -218,6 +218,7 @@ data IdeSlaveCommand = REPLCompletions String
218218 | TermNormalise [(Name, Bool)] Term
219219 | TermShowImplicits [(Name, Bool)] Term
220220 | TermNoImplicits [(Name, Bool)] Term
221+ | PrintDef String
221222
222223sexpToCommand :: SExp -> Maybe IdeSlaveCommand
223224sexpToCommand (SexpList (x:[])) = sexpToCommand x
@@ -260,6 +261,7 @@ sexpToCommand (SexpList [SymbolAtom "show-term-implicits", StringAtom encoded])
260261 Just (TermShowImplicits bnd tm)
261262sexpToCommand (SexpList [SymbolAtom "hide-term-implicits", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in
262263 Just (TermNoImplicits bnd tm)
264+sexpToCommand (SexpList [SymbolAtom "print-definition", StringAtom name]) = Just (PrintDef name)
263265sexpToCommand _ = Nothing
264266
265267parseMessage :: String -> Either Err (SExp, Integer)
src/Idris/REPL.hs+10
@@ -477,6 +477,16 @@ runIdeSlaveCommand h id orig fn modes (IdeSlave.TermShowImplicits bnd tm) =
477477 ideSlaveForceTermImplicits h id bnd True tm
478478runIdeSlaveCommand h id orig fn modes (IdeSlave.TermNoImplicits bnd tm) =
479479 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+
480490
481491-- | Show a term for IDESlave with the specified implicitness
482492ideSlaveForceTermImplicits :: Handle -> Integer -> [(Name, Bool)] -> Bool -> Term -> Idris ()