8d96041 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Annotate links with their URL

This allows frontends other than the console to display links with a special decoration. For example, the Emacs mode underlines the link text and makes it clickable, and the HTML output for :printdef uses the appropriate tag. The console still shows the link text parenthesized after the underlined link text.

commit8d96041781dac1c754a7546e6f951d7bdade87d9 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateMon 22 Jun 2015, 12:28 (11 years ago) parent67143bd

5 files changed+8−2

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+2 src/Idris/Core/TT.hs+1 src/Idris/Docstrings.hs+1−2 src/Idris/IdeMode.hs+1 src/Idris/Output.hs+3

src/Idris/AbsSyntaxTree.hs+2

@@ -1494,6 +1494,8 @@ consoleDecorate ist (AnnTerm _ _) = id

14941494consoleDecorate ist (AnnSearchResult _) = id

14951495consoleDecorate ist (AnnErr _) = id

14961496consoleDecorate ist (AnnNamespace _ _) = id

1497+consoleDecorate ist (AnnLink url) =

1498+ \txt -> Idris.Colours.colourise (IdrisColour Nothing True True False False) txt ++ " (" ++ url ++ ")"

14971499

14981500isPostulateName :: Name -> IState -> Bool

14991501isPostulateName n ist = S.member n (idris_postulates ist)

src/Idris/Core/TT.hs+1

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

175175 | AnnKeyword

176176 | AnnFC FC

177177 | AnnTextFmt TextFormatting

178+ | AnnLink String -- ^ A link to this URL

178179 | AnnTerm [(Name, Bool)] (TT Name) -- ^ pprint bound vars, original term

179180 | AnnSearchResult Ordering -- ^ more general, isomorphic, or more specific

180181 | AnnErr Err

src/Idris/Docstrings.hs+1−2

@@ -190,8 +190,7 @@ renderInline pp LineBreak = line

190190renderInline pp (Emph txt) = annotate (AnnTextFmt ItalicText) $ renderInlines pp txt

191191renderInline pp (Strong txt) = annotate (AnnTextFmt BoldText) $ renderInlines pp txt

192192renderInline pp (Code txt tm) = pp tm $ T.unpack txt

193−renderInline pp (Link body url title) = annotate (AnnTextFmt UnderlineText) (renderInlines pp body) <+>

194− parens (text $ T.unpack url)

193+renderInline pp (Link body url title) = annotate (AnnLink (T.unpack url)) (renderInlines pp body)

195194renderInline pp (Image body url title) = text "<image>" -- TODO

196195renderInline pp (Entity a) = text $ "<entity " ++ T.unpack a ++ ">" -- TODO

197196renderInline pp (RawHtml txt) = text "<html content>" --TODO

src/Idris/IdeMode.hs+1

@@ -148,6 +148,7 @@ instance SExpable OutputAnnotation where

148148 BoldText -> "bold"

149149 ItalicText -> "italic"

150150 UnderlineText -> "underline"

151+ toSExp (AnnLink url) = toSExp [(SymbolAtom "link-href", StringAtom url)]

151152 toSExp (AnnTerm bnd tm)

152153 | termSmallerThan 1000 tm = toSExp [(SymbolAtom "tt-term", StringAtom (encodeTerm bnd tm))]

153154 | otherwise = SexpList []

src/Idris/Output.hs+3

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

256256 decorate HTMLOutput (AnnSearchResult _) = id

257257 decorate HTMLOutput (AnnErr _) = id

258258 decorate HTMLOutput (AnnNamespace _ _) = id

259+ decorate HTMLOutput (AnnLink url) =

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

259261

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

261263 latex "IdrisType"

@@ -284,6 +286,7 @@ renderExternal fmt width doc

284286 decorate LaTeXOutput (AnnSearchResult _) = id

285287 decorate LaTeXOutput (AnnErr _) = id

286288 decorate LaTeXOutput (AnnNamespace _ _) = id

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

287290

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

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