ec0b043 · Idris-dev · git.iko.soy

docs/reference/ide-protocol.rst+6

compare with master

unifiedsplit

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

177 ``link-href``

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

179

180+ ``quasiquotation``

181+ states that the region is quasiquoted.

182+

183+ ``antiquotation``

184+ states that the region is antiquoted.

185+

180 ``tt-term``

186 ``tt-term``

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

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

182

188

src/Idris/Core/TT.hs+2

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

190+ | AnnAntiquote

189 deriving (Show, Eq)

191 deriving (Show, Eq)

190

192

191-- | Used for error reflection

193-- | Used for error reflection

src/Idris/IdeMode.hs+2

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

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

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

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

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

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

166

168

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

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

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

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

src/Idris/Output.hs+4

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

285 decorate HTMLOutput (AnnNamespace _ _) = id

286 decorate HTMLOutput (AnnLink url) =

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

288+ decorate HTMLOutput AnnQuasiquote = id

289+ decorate HTMLOutput AnnAntiquote = id

288

290

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

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

290 latex "IdrisType"

292 latex "IdrisType"

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

314 decorate LaTeXOutput (AnnErr _) = id

316 decorate LaTeXOutput (AnnErr _) = id

315 decorate LaTeXOutput (AnnNamespace _ _) = id

317 decorate LaTeXOutput (AnnNamespace _ _) = id

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

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

319+ decorate LaTeXOutput AnnQuasiquote = id

320+ decorate LaTeXOutput AnnAntiquote = id

317

321

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

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

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

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

src/Idris/ParseExpr.hs+3−1

@@ -656,7 +656,7 @@ quasiquote syn = do startFC <- 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)]

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

660 case g of

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

662 _ -> return ()

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

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

673 startFC <- symbolFC "~"

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

675+ endFC <- getFC

675 highlightP startFC AnnKeyword

676 highlightP startFC AnnKeyword

677+ highlightP (spanFC startFC endFC) AnnAntiquote

676 return $ PUnquote e

678 return $ PUnquote e

677 <?> "unquotation"

679 <?> "unquotation"

678

680