git.iko.soy/Idris-dev
on master help sign in
Merge pull request #910 from david-christiansen/ideslave-explicit-namespaces

IDESlave improvements: namespaces and docs

commit2afab0d17f74fe0e02f4387d921c4a24f2692749 authorEdwin Brady <edwin.brady@gmail.com> dateWed 19 Feb 2014, 23:30 (13 years ago) parent6d3863d6370ef3
2 files changed+21−1
compare with master
unifiedsplit
src/Idris/IdeSlave.hs+6 src/Idris/REPL.hs+15−1
src/Idris/IdeSlave.hs+6
@@ -89,6 +89,10 @@ instance SExpable OutputAnnotation where
8989 (SymbolAtom "implicit", BoolAtom imp)]
9090 toSExp AnnConstData = toSExp [(SymbolAtom "decor", SymbolAtom "data")]
9191 toSExp AnnConstType = toSExp [(SymbolAtom "decor", SymbolAtom "type")]
92+ toSExp (AnnFC (FC f l c)) = toSExp [(SymbolAtom "source-loc",
93+ ((SymbolAtom "filename", StringAtom f),
94+ (SymbolAtom "line", IntegerAtom (toInteger l)),
95+ (SymbolAtom "column", IntegerAtom (toInteger c))))]
9296
9397escape :: String -> String
9498escape = concatMap escapeChar
@@ -130,6 +134,7 @@ data IdeSlaveCommand = REPLCompletions String
130134 | MakeWithBlock Int String
131135 | ProofSearch Int String [String]
132136 | LoadFile String
137+ | DocsFor String
133138 deriving Show
134139
135140sexpToCommand :: SExp -> Maybe IdeSlaveCommand
@@ -147,6 +152,7 @@ sexpToCommand (SexpList [SymbolAtom "proof-search", IntegerAtom line, StringAtom
147152 where getHints = mapM (\h -> case h of
148153 StringAtom s -> Just s
149154 _ -> Nothing)
155+sexpToCommand (SexpList [SymbolAtom "docs-for", StringAtom name]) = Just (DocsFor name)
150156sexpToCommand _ = Nothing
151157
152158parseMessage :: String -> Either Err (SExp, Integer)
src/Idris/REPL.hs+15−1
@@ -41,6 +41,8 @@ import Idris.Core.Constraints
4141import IRTS.Compiler
4242import IRTS.CodegenCommon
4343
44+import Data.List.Split (splitOn)
45+
4446import Text.Trifecta.Result(Result(..))
4547
4648-- import RTS.SC
@@ -249,7 +251,14 @@ ideslave orig mods
249251 Just x -> iPrintError $ "didn't load " ++ filename
250252 ideslave orig [filename]
251253 Just (IdeSlave.TypeOf name) ->
252− process stdout "(ideslave)" (Check (PRef (FC "(ideslave)" 0 0) (sUN name)))
254+ case splitName name of
255+ Left err -> iPrintError err
256+ Right n -> process stdout "(ideslave)"
257+ (Check (PRef (FC "(ideslave)" 0 0) n))
258+ Just (IdeSlave.DocsFor name) ->
259+ case splitName name of
260+ Left err -> iPrintError err
261+ Right n -> process stdout "(ideslave)" (DocStr n)
253262 Just (IdeSlave.CaseSplit line name) ->
254263 process stdout fn (CaseSplitAt False line (sUN name))
255264 Just (IdeSlave.AddClause line name) ->
@@ -266,6 +275,11 @@ ideslave orig mods
266275 (\e -> do iPrintError $ show e))
267276 (\e -> do iPrintError $ show e)
268277 ideslave orig mods
278+ where splitName :: String -> Either String Name
279+ splitName s = case reverse $ splitOn "." s of
280+ [] -> Left ("Didn't understand name '" ++ s ++ "'")
281+ [n] -> Right $ sUN n
282+ (n:ns) -> Right $ sNS (sUN n) ns
269283
270284ideslaveProcess :: FilePath -> Command -> Idris ()
271285ideslaveProcess fn Help = process stdout fn Help