mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-11-11 14:57:30 +03:00
Parser-driven highlighting of quasiquoted regions
Now, quasiquotation and antiquotation regions are annotated by the parser, which can help editors.
This commit is contained in:
parent
2a4e82b2e0
commit
ec0b043055
@ -177,6 +177,12 @@ The following keys are available:
|
||||
``link-href``
|
||||
provides a URL that the corresponding text is a link to.
|
||||
|
||||
``quasiquotation``
|
||||
states that the region is quasiquoted.
|
||||
|
||||
``antiquotation``
|
||||
states that the region is antiquoted.
|
||||
|
||||
``tt-term``
|
||||
A serialized representation of the Idris core term corresponding to the region of text.
|
||||
|
||||
|
@ -186,6 +186,8 @@ data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe String) (Maybe St
|
||||
-- resolved. If a file path is present, then
|
||||
-- the namespace represents a module imported
|
||||
-- from that file.
|
||||
| AnnQuasiquote
|
||||
| AnnAntiquote
|
||||
deriving (Show, Eq)
|
||||
|
||||
-- | Used for error reflection
|
||||
|
@ -163,6 +163,8 @@ instance SExpable OutputAnnotation where
|
||||
toSExp $ [(SymbolAtom "namespace", StringAtom (intercalate "." (map T.unpack ns)))] ++
|
||||
[(SymbolAtom "decor", SymbolAtom $ if isJust file then "module" else "namespace")] ++
|
||||
maybeProps [("source-file", file)]
|
||||
toSExp AnnQuasiquote = toSExp [(SymbolAtom "quasiquotation", True)]
|
||||
toSExp AnnAntiquote = toSExp [(SymbolAtom "antiquotation", True)]
|
||||
|
||||
encodeTerm :: [(Name, Bool)] -> Term -> String
|
||||
encodeTerm bnd tm = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $
|
||||
|
@ -285,6 +285,8 @@ renderExternal fmt width doc
|
||||
decorate HTMLOutput (AnnNamespace _ _) = id
|
||||
decorate HTMLOutput (AnnLink url) =
|
||||
\txt -> "<a href=\"" ++ url ++ "\">" ++ txt ++ "</a>"
|
||||
decorate HTMLOutput AnnQuasiquote = id
|
||||
decorate HTMLOutput AnnAntiquote = id
|
||||
|
||||
decorate LaTeXOutput (AnnName _ (Just TypeOutput) _ _) =
|
||||
latex "IdrisType"
|
||||
@ -314,6 +316,8 @@ renderExternal fmt width doc
|
||||
decorate LaTeXOutput (AnnErr _) = id
|
||||
decorate LaTeXOutput (AnnNamespace _ _) = id
|
||||
decorate LaTeXOutput (AnnLink url) = (++ "(\\url{" ++ url ++ "})")
|
||||
decorate LaTeXOutput AnnQuasiquote = id
|
||||
decorate LaTeXOutput AnnAntiquote = id
|
||||
|
||||
tag cls docs str = "<span class=\""++cls++"\""++title++">" ++ str ++ "</span>"
|
||||
where title = maybe "" (\d->" title=\"" ++ d ++ "\"") docs
|
||||
|
@ -656,7 +656,7 @@ quasiquote syn = do startFC <- symbolFC "`("
|
||||
ty <- expr syn { inPattern = False } -- don't allow antiquotes
|
||||
return (ty, fc)
|
||||
endFC <- symbolFC ")"
|
||||
mapM_ (uncurry highlightP) [(startFC, AnnKeyword), (endFC, AnnKeyword)]
|
||||
mapM_ (uncurry highlightP) [(startFC, AnnKeyword), (endFC, AnnKeyword), (spanFC startFC endFC, AnnQuasiquote)]
|
||||
case g of
|
||||
Just (_, fc) -> highlightP fc AnnKeyword
|
||||
_ -> return ()
|
||||
@ -672,7 +672,9 @@ unquote :: SyntaxInfo -> IdrisParser PTerm
|
||||
unquote syn = do guard (syn_in_quasiquote syn > 0)
|
||||
startFC <- symbolFC "~"
|
||||
e <- simpleExpr syn { syn_in_quasiquote = syn_in_quasiquote syn - 1 }
|
||||
endFC <- getFC
|
||||
highlightP startFC AnnKeyword
|
||||
highlightP (spanFC startFC endFC) AnnAntiquote
|
||||
return $ PUnquote e
|
||||
<?> "unquotation"
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user