From 6ad14fb88669097e2b0159436ccdd3e41c3b486d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Am=C3=A9lia=20Liao?= 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