first commit

.gitignore

@@ -0,0 +1,2 @@
+/.stack-work
+/agda-reference-filter

LICENSE

@@ -0,0 +1,30 @@
+Copyright Abigail Magalhães (c) 2021
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Abigail Magalhães nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

README.md

@@ -0,0 +1,12 @@
+# agda-reference-filter
+
+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.
+
+```bash
+agda --html-highlight=auto --html example.lagda.md
+pandoc --filter agda-reference-filter -i example.md -o example.html
+```

Setup.hs

@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain

agda-reference-filter.cabal

@@ -0,0 +1,13 @@
+cabal-version: 2.2
+name:          agda-reference-filter
+version:       0.1.0.0
+
+executable agda-reference-filter
+  hs-source-dirs:      src
+  main-is:             Main.hs
+  default-language:    Haskell2010
+  build-depends:       base >= 4.7 && < 5
+                     , tagsoup
+                     , pandoc-types
+                     , unordered-containers
+                     , text

example.lagda.md

@@ -0,0 +1,6 @@
+This is a literate Agda file. This span - `span` - will be linked to the record below:
+
+```agda
+record span : Set where
+  constructor hey-look
+```

hie.yaml

@@ -0,0 +1,2 @@
+cradle:
+  stack:

src/Main.hs

@@ -0,0 +1,47 @@
+{-# LANGUAGE OverloadedStrings #-}
+module Main where
+
+import qualified Data.HashMap.Strict as HashMap
+import Data.HashMap.Strict (HashMap)
+import qualified Data.Text as T
+import Data.Text (Text)
+import Data.Maybe
+import Data.List
+
+import System.Environment
+import System.Exit
+
+import Text.Pandoc.Definition
+import Text.HTML.TagSoup
+import Text.Pandoc.Walk
+import Text.Pandoc.JSON
+
+
+main :: IO ()
+main = toJSONFilter linkDocument
+
+linkDocument :: Pandoc -> Pandoc
+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 _ x = x
+
+parseSymbolRefs :: [Block] -> HashMap Text Text
+parseSymbolRefs = go mempty . concat . mapMaybe getHTML where
+  getHTML (RawBlock (Format x) xs)
+    | x == "html" = Just (parseTags (T.unpack 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
+    | 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

stack.yaml

@@ -0,0 +1,5 @@
+resolver:
+  url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/18/13.yaml
+
+packages:
+- .

stack.yaml.lock

@@ -0,0 +1,13 @@
+# This file was autogenerated by Stack.
+# You should not edit this file by hand.
+# For more information, please see the documentation at:
+#   https://docs.haskellstack.org/en/stable/lock_files
+
+packages: []
+snapshots:
+- completed:
+    size: 586268
+    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/18/13.yaml
+    sha256: d9e658a22cfe8d87a64fdf219885f942fef5fe2bcb156a9800174911c5da2443
+  original:
+    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/18/13.yaml