ec0b043 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Parser-driven highlighting of quasiquoted regions

Now, quasiquotation and antiquotation regions are annotated by the parser, which can help editors.

commitec0b043055f1ffd1fb02f4f5a5f66d615b957c06 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateFri 10 Jul 2015, 11:57 (11 years ago) parent2a4e82b

5 files changed+17−1

compare with master

unifiedsplit

docs/reference/ide-protocol.rst+6 src/Idris/Core/TT.hs+2 src/Idris/IdeMode.hs+2 src/Idris/Output.hs+4 src/Idris/ParseExpr.hs+3−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/Core/TT.hs+2

@@ -186,6 +186,8 @@ 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+ | AnnQuasiquote

190+ | AnnAntiquote

189191 deriving (Show, Eq)

190192

191193-- | Used for error reflection

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+4

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

285285 decorate HTMLOutput (AnnNamespace _ _) = id

286286 decorate HTMLOutput (AnnLink url) =

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

288+ decorate HTMLOutput AnnQuasiquote = id

289+ decorate HTMLOutput AnnAntiquote = id

288290

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

290292 latex "IdrisType"

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

314316 decorate LaTeXOutput (AnnErr _) = id

315317 decorate LaTeXOutput (AnnNamespace _ _) = id

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

319+ decorate LaTeXOutput AnnQuasiquote = id

320+ decorate LaTeXOutput AnnAntiquote = id

317321

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

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

src/Idris/ParseExpr.hs+3−1

@@ -656,7 +656,7 @@ quasiquote syn = do startFC <- symbolFC "`("

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

657657 return (ty, fc)

658658 endFC <- symbolFC ")"

659− mapM_ (uncurry highlightP) [(startFC, AnnKeyword), (endFC, AnnKeyword)]

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

660660 case g of

661661 Just (_, fc) -> highlightP fc AnnKeyword

662662 _ -> return ()

@@ -672,7 +672,9 @@ unquote :: SyntaxInfo -> IdrisParser PTerm

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

673673 startFC <- symbolFC "~"

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

675+ endFC <- getFC

675676 highlightP startFC AnnKeyword

677+ highlightP (spanFC startFC endFC) AnnAntiquote

676678 return $ PUnquote e

677679 <?> "unquotation"

678680