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

git.iko.soy/Idris-dev

Initial parser-driven highlighting

For now, this provides highlighting for user-defined syntax extensions. Eventually, the parser will provide more information about the tokens and potentially the syntactic structure of the parsed code.

commit520f36765ed47c293d7e2f668059c6f1cf539b64 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateFri 10 Jul 2015, 10:44 (11 years ago) parent203945b

6 files changed+31−8

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+3−2 src/Idris/Core/TT.hs+3−3 src/Idris/Output.hs+7 src/Idris/ParseExpr.hs+5−2 src/Idris/ParseHelpers.hs+9 src/Idris/Parser.hs+4−1

src/Idris/AbsSyntaxTree.hs+3−2

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

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

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

244244 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

246247 }

247248

248249-- Required for parsers library, and therefore trifecta

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

330331 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

331332 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

332333 (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 [] [] []

334335

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

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

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

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

159159 show (FileFC f) = f

160160

161161-- | 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)

163163

164164-- | Text formatting output

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

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

166166

167167-- | Output annotations for pretty-printing

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

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

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

187187 -- the namespace represents a module imported

188188 -- from that file.

189− deriving Show

189+ deriving (Show, Eq)

190190

191191-- | Used for error reflection

192192data ErrorReportPart = TextPart String

src/Idris/Output.hs+7

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

196196 where ppTm = pprintDelab ist

197197 norm = normaliseAll (tt_ctxt ist) []

198198

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+

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

200207sendHighlighting highlights =

201208 do ist <- getIState

src/Idris/ParseExpr.hs+5−2

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

147147 ruleGroup _ _ = False

148148

149149 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

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

152154 return $ Just (n, SynTm tm)

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

154156 return $ Just (n, SynTm tm)

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

156158 return $ Just (n, SynBind b)

157− extensionSymbol (Symbol s) = do symbol s

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

160+ highlightP fc AnnKeyword

158161 return Nothing

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

160163 dropn n [] = []

src/Idris/ParseHelpers.hs+9

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

7979 parseString (runInnerParser (evalStateT p i))

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

8181

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

83+highlightP fc annot = do ist <- get

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

85+

8286noDocCommentHere :: String -> IdrisParser ()

8387noDocCommentHere msg =

8488 optional (do fc <- getFC

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

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

261265symbol = Tok.symbol

262266

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+

263272-- | Parses a reserved identifier

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

265274reserved = Tok.reserve idrisStyle

src/Idris/Parser.hs+4−1

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

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

9999moduleHeader = try (do docs <- optional docComment

100100 noArgs docs

101− reserved "module"

101+ modFC <- reservedFC "module"

102+ highlightP modFC AnnKeyword

102103 (i, ifc) <- identifier

103104 option ';' (lchar ';')

104105 let modName = moduleName i

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

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

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

14321433 reportParserWarnings

1434+ sendParserHighlighting

14331435

14341436 -- process and check module aliases

14351437 let modAliases = M.fromList

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

14801482 ibc_write ist

14811483 }

14821484 _ -> return ()

1485+ sendParserHighlighting

14831486

14841487 -- Parsing done, now process declarations

14851488