From 296e68025be53794472d11ce2824f39fb638cc0d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Abigail=20Magalh=C3=A3es?= Date: Thu, 7 Oct 2021 20:52:26 -0300 Subject: [PATCH] Allow control of span linking --- .gitignore | 6 ++++- README.md | 30 ++++++++++++++++++++-- example/example.html | 12 ++++++--- example/example.lagda.md | 10 ++++++-- example/example.md | 12 ++++++--- src/Main.hs | 55 ++++++++++++++++++++++++++++++++++------ 6 files changed, 106 insertions(+), 19 deletions(-) diff --git a/.gitignore b/.gitignore index 7ccfd92..256980c 100644 --- a/.gitignore +++ b/.gitignore @@ -1,2 +1,6 @@ /.stack-work -/agda-reference-filter \ No newline at end of file +/agda-reference-filter + +/example/Agda*.html +/example/*.agdai +/example/*.css \ No newline at end of file diff --git a/README.md b/README.md index b37dc27..a0a23f2 100644 --- a/README.md +++ b/README.md @@ -4,9 +4,35 @@ A Pandoc filter for linking Agda identifiers in inline code blocks. ## Usage -Compile your literate Agda file to Markdown (use `--html-highlight=auto`), then `pandoc --filter agda-reference-filter -i output.md -o output.html` to compile the Markdown to HTML. Inline code spans that are exactly the same as an identifier present in the raw HTML emitted by Agda (that is - either a definition or a reference) will be linked to the same place that Agda linked that identifier to. +The filter operates on Markdown files generated by Agda's built-in +literate programming support (use `--html-highlight=auto` to keep the +Markdown), then call Pandoc with the filter: ```bash agda --html-highlight=auto --html example.lagda.md pandoc --filter agda-reference-filter -i example.md -o example.html -``` \ No newline at end of file +``` + +The input file will be scanned, in source order, to build a variable +name - HTML element association. + +Only the first reference is counted: if you have two identifiers called +`go`, then `` `go` `` in Markdown will link to the first. + +### Controlling whether spans are linked + +Code spans in Markdown are only linked if they have the `agda` - **case +insensitive** - class. In Pandoc syntax, you can attach a class to a +code span like so: + +``` +`List`{.agda} +``` + +If you want a span to have the `agda` class but for it not to be linked, +add the `nolink` class. + +### Controlling what spans are linked to + +If a span has the `ident` attribute, then the value of that attribute +will be used as the identifier to link to instead of the span text. \ No newline at end of file diff --git a/example/example.html b/example/example.html index 78e1a4c..61ebba5 100644 --- a/example/example.html +++ b/example/example.html @@ -1,4 +1,10 @@ -

This is a literate Agda file. This span - span - will be linked to the record below:

-
record span : Set where
-  constructor hey-look
+

This is a literate Agda file.

+

Here’s some inline code:

+ +
record Record : Set where
+  constructor hey-look
 
diff --git a/example/example.lagda.md b/example/example.lagda.md index 8351131..67782f7 100644 --- a/example/example.lagda.md +++ b/example/example.lagda.md @@ -1,6 +1,12 @@ -This is a literate Agda file. This span - `span` - will be linked to the record below: +This is a literate Agda file. + +Here's some inline code: + +- This is a link to the record below: `Record`{.agda} +- This is not: `Record` +- This is a link with alternate text: `also a link`{.agda ident=Record} ```agda -record span : Set where +record Record : Set where constructor hey-look ``` \ No newline at end of file diff --git a/example/example.md b/example/example.md index 6e99f08..b7bed48 100644 --- a/example/example.md +++ b/example/example.md @@ -1,5 +1,11 @@ -This is a literate Agda file. This span - `span` - will be linked to the record below: +This is a literate Agda file. -
record span : Set where
-  constructor hey-look
+Here's some inline code:
+
+- This is a link to the record below: `Record`{.agda}
+- This is not: `Record`
+- This is a link with alternate text: `also a link`{.agda ident=Record}
+
+
record Record : Set where
+  constructor hey-look
 
\ No newline at end of file diff --git a/src/Main.hs b/src/Main.hs index 2ef1d45..349248e 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -25,23 +25,62 @@ linkDocument (Pandoc meta blocks) = let hm = parseSymbolRefs blocks in Pandoc meta (walk (link hm) blocks) -link :: HashMap Text Text -> Inline -> Inline -link hm (Code attrs xs) - | Just sp <- HashMap.lookup xs hm = RawInline (Format "html") sp +link :: HashMap Text Reference -> Inline -> Inline +link hm inline@(Code (_, classes, kv) text) + | isToBeLinked = + case HashMap.lookup identifier hm of + Just ref -> RawInline "html" (renderReference ref text) + Nothing -> inline + where + classes' = map T.toLower classes + + isToBeLinked = ("agda" `elem` classes') + && ("nolink" `notElem` classes') + + identifier = + case lookup "ident" kv of + Just id -> id + _ -> text link _ x = x -parseSymbolRefs :: [Block] -> HashMap Text Text +renderReference :: Reference -> Text -> Text +renderReference (Reference href cls) t = + renderTags [ TagOpen "pre" [("class", "Agda")] + , TagOpen "a" [("href", href), ("class", cls)] + , TagText t + , TagClose "a" + , TagClose "pre" + ] + +data Reference = + Reference { refHref :: Text + , refClass :: Text + } + deriving (Eq, Show) + +parseSymbolRefs :: [Block] -> HashMap Text Reference parseSymbolRefs = go mempty . concat . mapMaybe getHTML where + getHTML :: Block -> Maybe ([Tag Text]) getHTML (RawBlock (Format x) xs) - | x == "html" = Just (parseTags (T.unpack xs)) + | x == "html" = Just (parseTags xs) getHTML _ = Nothing - go map (TagOpen "a" meta:TagText t:TagClose "a":xs) - | Just id <- lookup "id" meta, Just cls <- lookup "class" meta - = go (HashMap.insert (T.pack t) (T.pack (renderTags tags)) map) xs + go :: HashMap Text Reference -> [Tag Text] -> HashMap Text Reference + go map (TagOpen a meta:TagText t:TagClose a':xs) + | a == "a" + , a' == a + , Just id <- lookup "id" meta + , Just cls <- lookup "class" meta + , Just href <- lookup "href" meta + = go (addIfNotPresent t (Reference href cls) map) xs + | otherwise = go map xs where tags = [ TagOpen "span" [("class", "Agda")], TagOpen "a" meta', TagText t, TagClose "a", TagClose "span" ] meta' = filter ((/= "id") . fst) meta + go map (_:xs) = go map xs go map [] = map + +addIfNotPresent :: Text -> v -> HashMap Text v -> HashMap Text v +addIfNotPresent = HashMap.insertWith (\_ old -> old) \ No newline at end of file