d61641d · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+12

@@ -538,6 +538,18 @@ isetPrompt p = do i <- getIState

538538 case idris_outputmode i of

539539 IdeSlave n -> runIO . putStrLn $ convSExp "set-prompt" p n

540540

541+-- | Tell clients how much was parsed and loaded

542+isetLoadedRegion :: Idris ()

543+isetLoadedRegion = do i <- getIState

544+ let span = idris_parsedSpan i

545+ case span of

546+ Just fc ->

547+ case idris_outputmode i of

548+ IdeSlave n ->

549+ runIO . putStrLn $

550+ convSExp "set-loaded-region" fc n

551+ Nothing -> return ()

552+

541553setLogLevel :: Int -> Idris ()

542554setLogLevel l = do i <- getIState

543555 let opts = idris_options i

src/Idris/AbsSyntaxTree.hs+3−1

@@ -174,6 +174,7 @@ data IState = IState {

174174 indent_stack :: [Int],

175175 brace_stack :: [Maybe Int],

176176 lastTokenSpan :: Maybe FC, -- ^ What was the span of the latest token parsed?

177+ idris_parsedSpan :: Maybe FC,

177178 hide_list :: [(Name, Maybe Accessibility)],

178179 default_access :: Accessibility,

179180 default_total :: Bool,

@@ -255,6 +256,7 @@ data IBCWrite = IBCFix FixDecl

255256 | IBCFunctionErrorHandler Name Name Name

256257 | IBCPostulate Name

257258 | IBCTotCheckErr FC String

259+ | IBCParsedRegion FC

258260 deriving Show

259261

260262-- | The initial state for the compiler

@@ -264,7 +266,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

264266 emptyContext emptyContext emptyContext emptyContext

265267 emptyContext emptyContext

266268 [] [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

267− [] [] Nothing [] Nothing [] [] Nothing [] Hidden False [] Nothing [] [] RawOutput

269+ [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] [] RawOutput

268270 True defaultTheme stdout [] (0, emptyContext) emptyContext M.empty

269271 AutomaticWidth S.empty Nothing Nothing

270272

src/Idris/IBC.hs+14−5

@@ -30,7 +30,7 @@ import Codec.Compression.Zlib (compress)

3030import Util.Zlib (decompressEither)

3131

3232ibcVersion :: Word8

33−ibcVersion = 72

33+ibcVersion = 73

3434

3535data IBCFile = IBCFile { ver :: Word8,

3636 sourcefile :: FilePath,

@@ -68,7 +68,8 @@ data IBCFile = IBCFile { ver :: Word8,

6868 ibc_function_errorhandlers :: [(Name, Name, Name)], -- fn, arg, handler

6969 ibc_metavars :: [(Name, (Maybe Name, Int, Bool))],

7070 ibc_patdefs :: [(Name, ([([Name], Term, Term)], [PTerm]))],

71− ibc_postulates :: [Name]

71+ ibc_postulates :: [Name],

72+ ibc_parsedSpan :: Maybe FC

7273 }

7374 deriving Show

7475{-!

@@ -76,7 +77,7 @@ deriving instance Binary IBCFile

7677!-}

7778

7879initIBC :: IBCFile

79−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

80+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing

8081

8182loadIBC :: FilePath -> Idris ()

8283loadIBC fp = do imps <- getImported

@@ -241,6 +242,7 @@ ibc i (IBCMetavar n) f =

241242 Just t -> return f { ibc_metavars = (n, t) : ibc_metavars f }

242243ibc i (IBCPostulate n) f = return f { ibc_postulates = n : ibc_postulates f }

243244ibc i (IBCTotCheckErr fc err) f = return f { ibc_totcheckfail = (fc, err) : ibc_totcheckfail f }

245+ibc i (IBCParsedRegion fc) f = return f { ibc_parsedSpan = Just fc }

244246

245247process :: IBCFile -> FilePath -> Idris ()

246248process i fn

@@ -285,6 +287,7 @@ process i fn

285287 pFunctionErrorHandlers (ibc_function_errorhandlers i)

286288 pMetavars (ibc_metavars i)

287289 pPostulates (ibc_postulates i)

290+ pParsedSpan (ibc_parsedSpan i)

288291

289292timestampOlder :: FilePath -> FilePath -> Idris ()

290293timestampOlder src ibc = do srct <- runIO $ getModificationTime src

@@ -298,6 +301,10 @@ pPostulates ns = do

298301 i <- getIState

299302 putIState i{ idris_postulates = idris_postulates i `S.union` S.fromList ns }

300303

304+pParsedSpan :: Maybe FC -> Idris ()

305+pParsedSpan fc = do ist <- getIState

306+ putIState ist { idris_parsedSpan = fc }

307+

301308pImports :: [FilePath] -> Idris ()

302309pImports fs

303310 = do mapM_ (\f -> do i <- getIState

@@ -1168,7 +1175,7 @@ instance Binary MetaInformation where

11681175 return (DataMI x1)

11691176

11701177instance Binary IBCFile where

1171− put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37)

1178+ put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38)

11721179 = {-# SCC "putIBCFile" #-}

11731180 do put x1

11741181 put x2

@@ -1207,6 +1214,7 @@ instance Binary IBCFile where

12071214 put x35

12081215 put x36

12091216 put x37

1217+ put x38

12101218

12111219 get

12121220 = do x1 <- get

@@ -1247,7 +1255,8 @@ instance Binary IBCFile where

12471255 x35 <- get

12481256 x36 <- get

12491257 x37 <- get

1250− return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37)

1258+ x38 <- get

1259+ return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38)

12511260 else return (initIBC { ver = x1 })

12521261

12531262instance Binary DataOpt where

src/Idris/IdeSlave.hs+10−6

@@ -121,16 +121,19 @@ instance SExpable OutputAnnotation where

121121 (SymbolAtom "doc-overview", StringAtom doc)] ++

122122 if not (null name) then [(SymbolAtom "name", StringAtom name)] else []

123123 toSExp AnnKeyword = toSExp [(SymbolAtom "decor", SymbolAtom "keyword")]

124− toSExp (AnnFC (FC f (sl, sc) (el, ec))) = toSExp [(SymbolAtom "source-loc",

125− ((SymbolAtom "filename", StringAtom f),

126− (SymbolAtom "start", IntegerAtom (toInteger sl), IntegerAtom (toInteger sc)),

127− (SymbolAtom "end", IntegerAtom (toInteger el), IntegerAtom (toInteger ec))))]

124+ toSExp (AnnFC fc) = toSExp [(SymbolAtom "source-loc", toSExp fc)]

128125 toSExp (AnnTextFmt fmt) = toSExp [(SymbolAtom "text-formatting", SymbolAtom format)]

129126 where format = case fmt of

130127 BoldText -> "bold"

131128 ItalicText -> "italic"

132129 UnderlineText -> "underline"

133130

131+instance SExpable FC where

132+ toSExp (FC f (sl, sc) (el, ec)) =

133+ toSExp ((SymbolAtom "filename", StringAtom f),

134+ (SymbolAtom "start", IntegerAtom (toInteger sl), IntegerAtom (toInteger sc)),

135+ (SymbolAtom "end", IntegerAtom (toInteger el), IntegerAtom (toInteger ec)))

136+

134137escape :: String -> String

135138escape = concatMap escapeChar

136139 where

@@ -173,7 +176,7 @@ data IdeSlaveCommand = REPLCompletions String

173176 | MakeWithBlock Int String

174177 | ProofSearch Bool Int String [String] (Maybe Int) -- ^^ Recursive?, line, name, hints, depth

175178 | MakeLemma Int String

176− | LoadFile String

179+ | LoadFile String (Maybe Int)

177180 | DocsFor String

178181 | Apropos String

179182 | GetOpts

@@ -186,7 +189,8 @@ sexpToCommand :: SExp -> Maybe IdeSlaveCommand

186189sexpToCommand (SexpList (x:[])) = sexpToCommand x

187190sexpToCommand (SexpList [SymbolAtom "interpret", StringAtom cmd]) = Just (Interpret cmd)

188191sexpToCommand (SexpList [SymbolAtom "repl-completions", StringAtom prefix]) = Just (REPLCompletions prefix)

189−sexpToCommand (SexpList [SymbolAtom "load-file", StringAtom filename]) = Just (LoadFile filename)

192+sexpToCommand (SexpList [SymbolAtom "load-file", StringAtom filename, IntegerAtom line]) = Just (LoadFile filename (Just (fromInteger line)))

193+sexpToCommand (SexpList [SymbolAtom "load-file", StringAtom filename]) = Just (LoadFile filename Nothing)

190194sexpToCommand (SexpList [SymbolAtom "type-of", StringAtom name]) = Just (TypeOf name)

191195sexpToCommand (SexpList [SymbolAtom "case-split", IntegerAtom line, StringAtom name]) = Just (CaseSplit (fromInteger line) name)

192196sexpToCommand (SexpList [SymbolAtom "add-clause", IntegerAtom line, StringAtom name]) = Just (AddClause (fromInteger line) name)

src/Idris/Parser.hs+6−2

@@ -132,6 +132,10 @@ prog syn = do whiteSpace

132132 case maxline syn of

133133 Nothing -> do notOpenBraces; eof

134134 _ -> return ()

135+ ist <- get

136+ fc <- getFC

137+ put ist { idris_parsedSpan = Just (FC (fc_fname fc) (0,0) (fc_end fc)),

138+ ibc_write = IBCParsedRegion fc : ibc_write ist }

135139 return c

136140

137141{-| Parses a top-level declaration

@@ -158,12 +162,12 @@ decl syn = do fc <- getFC

158162 -- if we're after maxline, stop here

159163 let continue = case maxline syn of

160164 Nothing -> True

161− Just l -> if fst (fc_end fc) > l

165+ Just l -> if fst (fc_end fc) > l

162166 then False

163167 else True

164168 if continue then do notEndBlock

165169 declBody

166− else fail "End of readable input"

170+ else fail "End of readable input"

167171 where declBody :: IdrisParser [PDecl]

168172 declBody = declBody'

169173 <|> using_ syn

src/Idris/REPL.hs+9−4

@@ -253,17 +253,22 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.REPLCompletions str) =

253253 IdeSlave.toSExp (map replacement compls,

254254 reverse unused)]

255255 runIO $ putStrLn $ IdeSlave.convSExp "return" good id

256−runIdeSlaveCommand id orig fn mods (IdeSlave.LoadFile filename) =

256+runIdeSlaveCommand id orig fn mods (IdeSlave.LoadFile filename toline) =

257257 do i <- getIState

258258 clearErr

259259 putIState (orig { idris_options = idris_options i,

260260 idris_outputmode = (IdeSlave id) })

261− loadInputs stdout [filename] Nothing

261+ loadInputs stdout [filename] toline

262262 isetPrompt (mkPrompt [filename])

263263 -- Report either success or failure

264264 i <- getIState

265265 case (errSpan i) of

266− Nothing -> iPrintResult $ "loaded " ++ filename

266+ Nothing -> let msg = maybe (IdeSlave.SexpList [IdeSlave.SymbolAtom "ok",

267+ IdeSlave.SexpList []])

268+ (\fc -> IdeSlave.SexpList [IdeSlave.SymbolAtom "ok",

269+ IdeSlave.toSExp fc])

270+ (idris_parsedSpan i)

271+ in runIO . putStrLn $ IdeSlave.convSExp "return" msg id

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

268273 ideslave orig [filename]

269274runIdeSlaveCommand id orig fn mods (IdeSlave.TypeOf name) =

@@ -1056,7 +1061,7 @@ loadInputs h inputs toline -- furthest line to read in input source files

10561061 tryLoad keepstate [] = warnTotality >> return ()

10571062 tryLoad keepstate (f : fs)

10581063 = do ist <- getIState

1059− let maxline

1064+ let maxline

10601065 = case toline of

10611066 Nothing -> Nothing

10621067 Just l -> case f of