520f367 · Idris-dev · git.iko.soy

src/Idris/AbsSyntaxTree.hs+3−2

compare with master

unifiedsplit

@@ -242,7 +242,8 @@ data IState = IState {

242 -- (instances appear twice; also as a funtion name)

243 idris_symbols :: M.Map Name Name, -- ^ Symbol table (preserves sharing of names)

244 idris_exports :: [Name], -- ^ Functions with ExportList

245− idris_highlightedRegions :: [(FC, OutputAnnotation)] -- ^ Highlighting information to output

245+ idris_highlightedRegions :: [(FC, OutputAnnotation)], -- ^ Highlighting information to output

246+ idris_parserHighlights :: [(FC, OutputAnnotation)] -- ^ Highlighting information from the parser

246 }

247 }

247

248

248-- Required for parsers library, and therefore trifecta

249-- Required for parsers library, and therefore trifecta

@@ -330,7 +331,7 @@ idrisInit = IState initContext S.empty []

330 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

331 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

331 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

332 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

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

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

333− AutomaticWidth S.empty S.empty [] Nothing Nothing [] [] M.empty [] []

334+ AutomaticWidth S.empty S.empty [] Nothing Nothing [] [] M.empty [] [] []

334

335

335-- | The monad for the main REPL - reading and processing files and updating

336-- | The monad for the main REPL - reading and processing files and updating

336-- global state (hence the IO inner monad).

337-- global state (hence the IO inner monad).

src/Idris/Core/TT.hs+3−3

@@ -159,10 +159,10 @@ instance Show FC where

159 show (FileFC f) = f

160

161-- | Output annotation for pretty-printed name - decides colour

162−data NameOutput = TypeOutput | FunOutput | DataOutput | MetavarOutput | PostulateOutput deriving Show

162+data NameOutput = TypeOutput | FunOutput | DataOutput | MetavarOutput | PostulateOutput deriving (Show, Eq)

163

164-- | Text formatting output

165−data TextFormatting = BoldText | ItalicText | UnderlineText deriving Show

165+data TextFormatting = BoldText | ItalicText | UnderlineText deriving (Show, Eq)

166

167-- | Output annotations for pretty-printing

168data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe String) (Maybe String)

@@ -186,7 +186,7 @@ data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe String) (Maybe St

186 -- resolved. If a file path is present, then

187 -- the namespace represents a module imported

188 -- from that file.

189− deriving Show

189+ deriving (Show, Eq)

190

191-- | Used for error reflection

192data ErrorReportPart = TextPart String

src/Idris/Output.hs+7

@@ -196,6 +196,13 @@ prettyDocumentedIst ist (name, ty, docs) =

196 where ppTm = pprintDelab ist

197 norm = normaliseAll (tt_ctxt ist) []

198

199+sendParserHighlighting :: Idris ()

200+sendParserHighlighting =

201+ do ist <- getIState

202+ let hs = nub $ idris_parserHighlights ist

203+ sendHighlighting hs

204+ putIState ist {idris_parserHighlights = []}

205+

199sendHighlighting :: [(FC, OutputAnnotation)] -> Idris ()

206sendHighlighting :: [(FC, OutputAnnotation)] -> Idris ()

200sendHighlighting highlights =

207sendHighlighting highlights =

201 do ist <- getIState

208 do ist <- getIState

src/Idris/ParseExpr.hs+5−2

@@ -147,14 +147,17 @@ extension syn ns rules =

147 ruleGroup _ _ = False

148

149 extensionSymbol :: SSymbol -> IdrisParser (Maybe (Name, SynMatch))

150− extensionSymbol (Keyword n) = do reserved (show n); return Nothing

150+ extensionSymbol (Keyword n) = do fc <- reservedFC (show n)

151+ highlightP fc AnnKeyword

152+ return Nothing

151 extensionSymbol (Expr n) = do tm <- expr syn

153 extensionSymbol (Expr n) = do tm <- expr syn

152 return $ Just (n, SynTm tm)

154 return $ Just (n, SynTm tm)

153 extensionSymbol (SimpleExpr n) = do tm <- simpleExpr syn

155 extensionSymbol (SimpleExpr n) = do tm <- simpleExpr syn

154 return $ Just (n, SynTm tm)

156 return $ Just (n, SynTm tm)

155 extensionSymbol (Binding n) = do b <- fst <$> name

157 extensionSymbol (Binding n) = do b <- fst <$> name

156 return $ Just (n, SynBind b)

158 return $ Just (n, SynBind b)

157− extensionSymbol (Symbol s) = do symbol s

159+ extensionSymbol (Symbol s) = do fc <- symbolFC s

160+ highlightP fc AnnKeyword

158 return Nothing

161 return Nothing

159 dropn :: Name -> [(Name, a)] -> [(Name, a)]

162 dropn :: Name -> [(Name, a)] -> [(Name, a)]

160 dropn n [] = []

163 dropn n [] = []

src/Idris/ParseHelpers.hs+9

@@ -79,6 +79,10 @@ runparser p i inputname =

79 parseString (runInnerParser (evalStateT p i))

80 (Directed (UTF8.fromString inputname) 0 0 0 0)

81

82+highlightP :: FC -> OutputAnnotation -> IdrisParser ()

83+highlightP fc annot = do ist <- get

84+ put ist { idris_parserHighlights = (fc, annot) : idris_parserHighlights ist}

85+

82noDocCommentHere :: String -> IdrisParser ()

86noDocCommentHere :: String -> IdrisParser ()

83noDocCommentHere msg =

87noDocCommentHere msg =

84 optional (do fc <- getFC

88 optional (do fc <- getFC

@@ -260,6 +264,11 @@ lchar = token . char

260symbol :: MonadicParsing m => String -> m String

264symbol :: MonadicParsing m => String -> m String

261symbol = Tok.symbol

265symbol = Tok.symbol

262

266

267+symbolFC :: MonadicParsing m => String -> m FC

268+symbolFC str = do (FC file (l, c) _) <- getFC

269+ Tok.symbol str

270+ return $ FC file (l, c) (l, c + length str)

271+

263-- | Parses a reserved identifier

272-- | Parses a reserved identifier

264reserved :: MonadicParsing m => String -> m ()

273reserved :: MonadicParsing m => String -> m ()

265reserved = Tok.reserve idrisStyle

274reserved = Tok.reserve idrisStyle

src/Idris/Parser.hs+4−1

@@ -98,7 +98,8 @@ import System.IO

98moduleHeader :: IdrisParser (Maybe (Docstring ()), [String], [(FC, OutputAnnotation)])

99moduleHeader = try (do docs <- optional docComment

100 noArgs docs

101− reserved "module"

101+ modFC <- reservedFC "module"

102+ highlightP modFC AnnKeyword

102 (i, ifc) <- identifier

103 (i, ifc) <- identifier

103 option ';' (lchar ';')

104 option ';' (lchar ';')

104 let modName = moduleName i

105 let modName = moduleName i

@@ -1430,6 +1431,7 @@ loadSource lidr f toline

1430 sendHighlighting [(nfc, AnnNamespace ns srcFnAbs)])

1431 sendHighlighting [(nfc, AnnNamespace ns srcFnAbs)])

1431 [(re, fn, ns, nfc) | ImportInfo re fn _ ns _ nfc <- imports]

1432 [(re, fn, ns, nfc) | ImportInfo re fn _ ns _ nfc <- imports]

1432 reportParserWarnings

1433 reportParserWarnings

1434+ sendParserHighlighting

1433

1435

1434 -- process and check module aliases

1436 -- process and check module aliases

1435 let modAliases = M.fromList

1437 let modAliases = M.fromList

@@ -1480,6 +1482,7 @@ loadSource lidr f toline

1480 ibc_write ist

1482 ibc_write ist

1481 }

1483 }

1482 _ -> return ()

1484 _ -> return ()

1485+ sendParserHighlighting

1483

1486

1484 -- Parsing done, now process declarations

1487 -- Parsing done, now process declarations

1485

1488