2afab0d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #910 from david-christiansen/ideslave-explicit-namespaces

2afab0dEdwin Brady13 years ago

src/Idris/IdeSlave.hs+6

compare with master

unifiedsplit

@@ -89,6 +89,10 @@ instance SExpable OutputAnnotation where

89 (SymbolAtom "implicit", BoolAtom imp)]

90 toSExp AnnConstData = toSExp [(SymbolAtom "decor", SymbolAtom "data")]

91 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))))]

93escape :: String -> String

97escape :: String -> String

94escape = concatMap escapeChar

98escape = concatMap escapeChar

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

130 | MakeWithBlock Int String

134 | MakeWithBlock Int String

131 | ProofSearch Int String [String]

135 | ProofSearch Int String [String]

132 | LoadFile String

136 | LoadFile String

137+ | DocsFor String

133 deriving Show

138 deriving Show

134

139

135sexpToCommand :: SExp -> Maybe IdeSlaveCommand

140sexpToCommand :: SExp -> Maybe IdeSlaveCommand

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

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

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

148 StringAtom s -> Just s

153 StringAtom s -> Just s

149 _ -> Nothing)

154 _ -> Nothing)

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

150sexpToCommand _ = Nothing

156sexpToCommand _ = Nothing

151

157

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

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

src/Idris/REPL.hs+15−1

@@ -41,6 +41,8 @@ import Idris.Core.Constraints

41import IRTS.Compiler

42import IRTS.CodegenCommon

44+import Data.List.Split (splitOn)

45+

44import Text.Trifecta.Result(Result(..))

46import Text.Trifecta.Result(Result(..))

46-- import RTS.SC

48-- import RTS.SC

@@ -249,7 +251,14 @@ ideslave orig mods

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

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

250 ideslave orig [filename]

252 ideslave orig [filename]

251 Just (IdeSlave.TypeOf name) ->

253 Just (IdeSlave.TypeOf name) ->

254+ case splitName name of

255+ Left err -> iPrintError err

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

252− process stdout "(ideslave)" (Check (PRef (FC "(ideslave)" 0 0) (sUN name)))

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)

253 Just (IdeSlave.CaseSplit line name) ->

262 Just (IdeSlave.CaseSplit line name) ->

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

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

255 Just (IdeSlave.AddClause line name) ->

264 Just (IdeSlave.AddClause line name) ->

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

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

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

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

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

268 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

269

283

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

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

271ideslaveProcess fn Help = process stdout fn Help

285ideslaveProcess fn Help = process stdout fn Help