From bfb12cd6866efe680059be5666d6f5da1226612b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Am=C3=A9lia=20Liao?= Date: Thu, 7 Oct 2021 18:58:24 -0300 Subject: [PATCH] first commit --- .gitignore | 2 ++ LICENSE | 30 +++++++++++++++++++++++ README.md | 12 ++++++++++ Setup.hs | 2 ++ agda-reference-filter.cabal | 13 ++++++++++ example.lagda.md | 6 +++++ hie.yaml | 2 ++ src/Main.hs | 47 +++++++++++++++++++++++++++++++++++++ stack.yaml | 5 ++++ stack.yaml.lock | 13 ++++++++++ 10 files changed, 132 insertions(+) create mode 100644 .gitignore create mode 100644 LICENSE create mode 100644 README.md create mode 100644 Setup.hs create mode 100644 agda-reference-filter.cabal create mode 100644 example.lagda.md create mode 100644 hie.yaml create mode 100644 src/Main.hs create mode 100644 stack.yaml create mode 100644 stack.yaml.lock diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..7ccfd92 --- /dev/null +++ b/.gitignore @@ -0,0 +1,2 @@ +/.stack-work +/agda-reference-filter \ No newline at end of file diff --git a/LICENSE b/LICENSE new file mode 100644 index 0000000..ca46626 --- /dev/null +++ b/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. \ No newline at end of file diff --git a/README.md b/README.md new file mode 100644 index 0000000..b37dc27 --- /dev/null +++ b/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 +``` \ No newline at end of file diff --git a/Setup.hs b/Setup.hs new file mode 100644 index 0000000..9a994af --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/agda-reference-filter.cabal b/agda-reference-filter.cabal new file mode 100644 index 0000000..f85a7b4 --- /dev/null +++ b/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 diff --git a/example.lagda.md b/example.lagda.md new file mode 100644 index 0000000..8351131 --- /dev/null +++ b/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 +``` \ No newline at end of file diff --git a/hie.yaml b/hie.yaml new file mode 100644 index 0000000..4ef275e --- /dev/null +++ b/hie.yaml @@ -0,0 +1,2 @@ +cradle: + stack: diff --git a/src/Main.hs b/src/Main.hs new file mode 100644 index 0000000..2ef1d45 --- /dev/null +++ b/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 diff --git a/stack.yaml b/stack.yaml new file mode 100644 index 0000000..17601fd --- /dev/null +++ b/stack.yaml @@ -0,0 +1,5 @@ +resolver: + url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/18/13.yaml + +packages: +- . \ No newline at end of file diff --git a/stack.yaml.lock b/stack.yaml.lock new file mode 100644 index 0000000..659abd6 --- /dev/null +++ b/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