b709748 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #2428 from david-christiansen/parser-highlights

Parser highlights

commitb709748ffcc7beed43982a8fb047cb6079fc916a authorDavid Christiansen <david@davidchristiansen.dk> dateFri 10 Jul 2015, 13:29 (11 years ago) parent9a7f7d9 ec0b043

8 files changed+62−15

compare with master

unifiedsplit

docs/reference/ide-protocol.rst+6 src/Idris/AbsSyntaxTree.hs+3−2 src/Idris/Core/TT.hs+5−3 src/Idris/IdeMode.hs+2 src/Idris/Output.hs+13 src/Idris/ParseExpr.hs+20−9 src/Idris/ParseHelpers.hs+9 src/Idris/Parser.hs+4−1

docs/reference/ide-protocol.rst+6

@@ -177,6 +177,12 @@ The following keys are available:

177177 ``link-href``

178178 provides a URL that the corresponding text is a link to.

179179

180+ ``quasiquotation``

181+ states that the region is quasiquoted.

182+

183+ ``antiquotation``

184+ states that the region is antiquoted.

185+

180186 ``tt-term``

181187 A serialized representation of the Idris core term corresponding to the region of text.

182188

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+5−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,9 @@ 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+ | AnnQuasiquote

190+ | AnnAntiquote

191+ deriving (Show, Eq)

190192

191193-- | Used for error reflection

192194data ErrorReportPart = TextPart String

src/Idris/IdeMode.hs+2

@@ -163,6 +163,8 @@ instance SExpable OutputAnnotation where

163163 toSExp $ [(SymbolAtom "namespace", StringAtom (intercalate "." (map T.unpack ns)))] ++

164164 [(SymbolAtom "decor", SymbolAtom $ if isJust file then "module" else "namespace")] ++

165165 maybeProps [("source-file", file)]

166+ toSExp AnnQuasiquote = toSExp [(SymbolAtom "quasiquotation", True)]

167+ toSExp AnnAntiquote = toSExp [(SymbolAtom "antiquotation", True)]

166168

167169encodeTerm :: [(Name, Bool)] -> Term -> String

168170encodeTerm bnd tm = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $

src/Idris/Output.hs+13

@@ -196,6 +196,15 @@ 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 = map unwrap . nub . map wrap $ idris_parserHighlights ist

203+ sendHighlighting hs

204+ putIState ist {idris_parserHighlights = []}

205+ where wrap (fc, a) = (FC' fc, a)

206+ unwrap (fc', a) = (unwrapFC fc', a)

207+

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

200209sendHighlighting highlights =

201210 do ist <- getIState

@@ -276,6 +285,8 @@ renderExternal fmt width doc

276285 decorate HTMLOutput (AnnNamespace _ _) = id

277286 decorate HTMLOutput (AnnLink url) =

278287 \txt -> "<a href=\"" ++ url ++ "\">" ++ txt ++ "</a>"

288+ decorate HTMLOutput AnnQuasiquote = id

289+ decorate HTMLOutput AnnAntiquote = id

279290

280291 decorate LaTeXOutput (AnnName _ (Just TypeOutput) _ _) =

281292 latex "IdrisType"

@@ -305,6 +316,8 @@ renderExternal fmt width doc

305316 decorate LaTeXOutput (AnnErr _) = id

306317 decorate LaTeXOutput (AnnNamespace _ _) = id

307318 decorate LaTeXOutput (AnnLink url) = (++ "(\\url{" ++ url ++ "})")

319+ decorate LaTeXOutput AnnQuasiquote = id

320+ decorate LaTeXOutput AnnAntiquote = id

308321

309322 tag cls docs str = "<span class=\""++cls++"\""++title++">" ++ str ++ "</span>"

310323 where title = maybe "" (\d->" title=\"" ++ d ++ "\"") docs

src/Idris/ParseExpr.hs+20−9

@@ -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 [] = []

@@ -645,14 +648,19 @@ constraintArg syn = do symbol "@{"

645648

646649-}

647650quasiquote :: SyntaxInfo -> IdrisParser PTerm

648−quasiquote syn = do symbol "`("

651+quasiquote syn = do startFC <- symbolFC "`("

649652 e <- expr syn { syn_in_quasiquote = (syn_in_quasiquote syn) + 1 ,

650653 inPattern = False }

651− g <- optional $ do

652− symbol ":"

653− expr syn { inPattern = False } -- don't allow antiquotes

654− symbol ")"

655− return $ PQuasiquote e g

654+ g <- optional $

655+ do fc <- symbolFC ":"

656+ ty <- expr syn { inPattern = False } -- don't allow antiquotes

657+ return (ty, fc)

658+ endFC <- symbolFC ")"

659+ mapM_ (uncurry highlightP) [(startFC, AnnKeyword), (endFC, AnnKeyword), (spanFC startFC endFC, AnnQuasiquote)]

660+ case g of

661+ Just (_, fc) -> highlightP fc AnnKeyword

662+ _ -> return ()

663+ return $ PQuasiquote e (fst <$> g)

656664 <?> "quasiquotation"

657665

658666{-| Parses an unquoting inside a quasiquotation (for building reflected terms using the elaborator)

@@ -662,8 +670,11 @@ quasiquote syn = do symbol "`("

662670-}

663671unquote :: SyntaxInfo -> IdrisParser PTerm

664672unquote syn = do guard (syn_in_quasiquote syn > 0)

665− symbol "~"

673+ startFC <- symbolFC "~"

666674 e <- simpleExpr syn { syn_in_quasiquote = syn_in_quasiquote syn - 1 }

675+ endFC <- getFC

676+ highlightP startFC AnnKeyword

677+ highlightP (spanFC startFC endFC) AnnAntiquote

667678 return $ PUnquote e

668679 <?> "unquotation"

669680

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