71b477b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Add IDESlave command for getting documentation

71b477bDavid Raymond Christiansen13 years ago

src/Idris/IdeSlave.hs+2

compare with master

unifiedsplit

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

130 | MakeWithBlock Int String

131 | ProofSearch Int String [String]

132 | LoadFile String

133+ | DocsFor String

133 deriving Show

134 deriving Show

134

135

135sexpToCommand :: SExp -> Maybe IdeSlaveCommand

136sexpToCommand :: SExp -> Maybe IdeSlaveCommand

@@ -147,6 +148,7 @@ sexpToCommand (SexpList [SymbolAtom "proof-search", IntegerAtom line, StringAtom

147 where getHints = mapM (\h -> case h of

148 where getHints = mapM (\h -> case h of

148 StringAtom s -> Just s

149 StringAtom s -> Just s

149 _ -> Nothing)

150 _ -> Nothing)

151+sexpToCommand (SexpList [SymbolAtom "docs-for", StringAtom name]) = Just (DocsFor name)

150sexpToCommand _ = Nothing

152sexpToCommand _ = Nothing

151

153

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

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

src/Idris/REPL.hs+13−6

@@ -251,12 +251,14 @@ ideslave orig mods

251 Just x -> iPrintError $ "didn't load " ++ filename

252 ideslave orig [filename]

253 Just (IdeSlave.TypeOf name) ->

254− case reverse $ splitOn "." name of

254+ case splitName name of

255− [] -> iPrintError ("Didn't understand name '" ++ name ++ "'")

255+ Left err -> iPrintError err

256− [n] -> process stdout "(ideslave)"

256+ Right n -> process stdout "(ideslave)"

257− (Check (PRef (FC "(ideslave)" 0 0) (sUN n)))

257+ (Check (PRef (FC "(ideslave)" 0 0) n))

258+ Just (IdeSlave.DocsFor name) ->

259+ case splitName name of

260+ Left err -> iPrintError err

258− (n:ns) -> process stdout "(ideslave)"

261+ Right n -> process stdout "(ideslave)" (DocStr n)

259− (Check (PRef (FC "(ideslave)" 0 0) (sNS (sUN n) ns)))

260 Just (IdeSlave.CaseSplit line name) ->

262 Just (IdeSlave.CaseSplit line name) ->

261 process stdout fn (CaseSplitAt False line (sUN name))

263 process stdout fn (CaseSplitAt False line (sUN name))

262 Just (IdeSlave.AddClause line name) ->

264 Just (IdeSlave.AddClause line name) ->

@@ -273,6 +275,11 @@ ideslave orig mods

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

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

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

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

275 ideslave orig mods

277 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

276

283

277ideslaveProcess :: FilePath -> Command -> Idris ()

284ideslaveProcess :: FilePath -> Command -> Idris ()

278ideslaveProcess fn Help = process stdout fn Help

285ideslaveProcess fn Help = process stdout fn Help