agda · dannypsnl · Dec 15, 2025 · Dec 15, 2025 · Dec 15, 2025 · Dec 15, 2025
diff --git a/Agda.cabal b/Agda.cabal
@@ -471,6 +471,7 @@ library
     , async                >= 2.2.4     && < 2.3
     , base                 >= 4.16.4.0  && < 4.22
     , blaze-html           >= 0.9.1.2   && < 0.10
+    , blaze-markup         >= 0.8       && < 0.9
     , boxes                >= 0.1.5     && < 0.2
     , bytestring           >= 0.11.4.0  && < 0.13
     , case-insensitive     >= 1.2.1.0   && < 1.3
@@ -587,6 +588,7 @@ library
       Agda.Interaction.Highlighting.HTML
       Agda.Interaction.Highlighting.HTML.Backend
       Agda.Interaction.Highlighting.HTML.Base
+      Agda.Interaction.Highlighting.HTML.Forester
       Agda.Interaction.Highlighting.JSON
       Agda.Interaction.Highlighting.LaTeX
       Agda.Interaction.Highlighting.LaTeX.Backend

diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -250,6 +250,8 @@ Interaction and emacs mode
 Backends
 --------
 
+* `agda --html --html-highlight=code example.lagda.tree` now produces `html/example.tree`, which Forester can consume directly - no external tools needed.
+
 * New option `--ghc-trace` for GHC Backend to instrument code
   such that the Agda name of the function is printed to `stderr`
   whenever a function is entered.

diff --git a/doc/user-manual/tools/literate-programming.rst b/doc/user-manual/tools/literate-programming.rst
@@ -207,15 +207,13 @@ Literate Forester
 Files ending in :file:`.lagda.tree` are interpreted as literate
 Forester_ files. Literate forester uses ```\agda{...}``` for code blocks.
 
-You will need the postprocessor agda-tree_ to convert ``html/*.tree`` to a valid forester tree.
+  * Run ``agda --html --html-highlight=code example.lagda.tree`` to generate ``html/example.tree``.
+  * Add ``html/`` to the ``trees`` list in ``forest.toml`` so Forester can find the generated trees.
+  * Modify ``theme/tree.xsl`` of your forester project to include ``Agda.css`` in the linked stylesheets.
 
-  * ``agda --html --html-highlight=code example.lagda.tree`` will produce the file ``html/example.tree``.
-  * Run ``agda-tree build`` at where ``html/`` is located, this will produce subdirectory ``trees/`` there.
-  * Add ``trees/`` to ``forest.toml``.
-  * Add ``html/`` to ``forest.toml`` as assets.
-  * Modify ``theme/tree.xsl`` of your forester project, adding ``Agda.css`` to the linked styles.
+Running ``forester build`` produce file ``output/example/index.xml``.
 
-Running ``forester build`` should now produce file ``example.xml`` with Agda syntax highlighting.
+  * Run ``cp html/Agda.css output/``, now you get Agda syntax highlighting.
 
 .. code-block:: text
 
@@ -234,6 +232,9 @@ Running ``forester build`` should now produce file ``example.xml`` with Agda syn
     suc  : ℕ → ℕ
    }
 
+* Self-link issue with Agda + Forester: When compiling ``.lagda.tree`` files, Agda generates links to local definitions using the module name (e.g., ``bool.html#232``). However, Forester outputs pages as ``output/bool/index.html``. This mismatch causes self-referential links to resolve to ``bool/bool.html#232`` instead of ``#232`` on the current page, resulting in 404s. This cannot be fixed in Agda's HTML backend - it has no awareness of Forester's output structure. A post-processing script is needed: for each generated page, copy ``output/i/index.html`` to ``output/i/i.html`` so the incorrect paths become valid redirects.
+* A similar problem occurs with references to Agda modules not compiled as part of your forest - whether standard library modules or local ``.agda`` files without corresponding trees. A script could rewrite these as root-relative paths (e.g., ``/Agda.Primitive.html#388``), which works if you host at a domain root. But this isn't general - on GitHub Pages, for example, your site lives at ``your-id.github.io/your-repo/``, so the correct path would be ``/your-repo/Agda.Primitive.html#388`` - requiring the script to know your deployment prefix. Either way, you also need to copy the generated HTML files from ``html/`` to your output directory - Forester won't include them automatically.
+
 .. _TeX: http://tug.org/
 .. _reStructuredText: http://docutils.sourceforge.io/rst.html
 .. _Markdown: https://daringfireball.net/projects/markdown/
@@ -242,6 +243,5 @@ Running ``forester build`` should now produce file ``example.xml`` with Agda syn
 .. _Forester: https://sr.ht/~jonsterling/forester/
 
 .. _lhs2TeX: https://www.andres-loeh.de/lhs2tex/
-.. _agda-tree: https://github.com/dannypsnl/agda-tree
 .. _Sphinx: http://www.sphinx-doc.org/en/stable/
 .. _Pandoc: https://pandoc.org/
diff --git a/src/full/Agda/Interaction/Highlighting/HTML/Base.hs b/src/full/Agda/Interaction/Highlighting/HTML/Base.hs
@@ -50,6 +50,7 @@ import Text.Blaze.Html.Renderer.Text ( renderHtml )
   -- The defined operator (!!) attaches a list of such Attributes
 
 import Agda.Interaction.Highlighting.Precise hiding (toList)
+import Agda.Interaction.Highlighting.HTML.Forester
 
 import Agda.Syntax.Common
 import Agda.Syntax.TopLevelModuleName
@@ -182,7 +183,7 @@ renderSourceFile opts = renderSourcePage
   highlightOccur = htmlOptHighlightOccurrences opts
   htmlHighlight = htmlOptHighlight opts
   renderSourcePage (HtmlInputSourceFile moduleName fileType sourceCode hinfo) =
-    page cssFile highlightOccur onlyCode moduleName pageContents
+    page cssFile highlightOccur onlyCode fileType moduleName pageContents
     where
       tokens = tokenStream sourceCode hinfo
       onlyCode = highlightOnlyCode htmlHighlight fileType
@@ -242,19 +243,25 @@ h !! as = h ! mconcat as
 page :: FilePath              -- ^ URL to the CSS file.
      -> Bool                  -- ^ Highlight occurrences
      -> Bool                  -- ^ Whether to reserve literate
+     -> FileType              -- ^ Type of file
      -> TopLevelModuleName    -- ^ Module to be highlighted.
      -> Html
      -> Text
 page css
      highlightOccurrences
      htmlHighlight
+     fileType
      modName
      pageContent =
-  renderHtml $ if htmlHighlight
-               then pageContent
-               else Html5.docTypeHtml $ hdr <> rest
+  renderF $ if htmlHighlight
+            then pageContent
+            else Html5.docTypeHtml $ hdr <> rest
   where
 
+    renderF = case fileType of
+      TreeFileType -> renderForesterHtml
+      _ -> renderHtml
+
     hdr = Html5.head $ mconcat
       [ Html5.meta !! [ Attr.charset "utf-8" ]
       , Html5.title (toHtml . render $ pretty modName)

diff --git a/src/full/Agda/Interaction/Highlighting/HTML/Forester.hs b/src/full/Agda/Interaction/Highlighting/HTML/Forester.hs
@@ -0,0 +1,147 @@
+module Agda.Interaction.Highlighting.HTML.Forester
+  ( renderForesterHtml,
+  )
+where
+
+import Data.ByteString (ByteString)
+import Data.ByteString qualified as S (isInfixOf)
+import Data.List (isInfixOf)
+import Data.Monoid (mappend, mempty)
+import Data.Text (Text)
+import Data.Text qualified as T
+import Data.Text.Encoding (decodeUtf8)
+import Data.Text.Lazy qualified as L
+import Data.Text.Lazy.Builder (Builder)
+import Data.Text.Lazy.Builder qualified as B
+import Text.Blaze.Html5 (Html)
+import Text.Blaze.Internal
+  ( ChoiceString (..),
+    MarkupM (..),
+    StaticString (getText),
+  )
+
+fromChoiceString ::
+  -- | Decoder for bytestrings
+  (ByteString -> Text) ->
+  -- | String to render
+  ChoiceString ->
+  -- | Resulting builder
+  Builder
+fromChoiceString _ (Static s) = B.fromText $ getText s
+fromChoiceString _ (String s) = B.fromText $ T.pack s
+fromChoiceString _ (Text s) = B.fromText s
+fromChoiceString d (ByteString s) = B.fromText $ d s
+fromChoiceString d (PreEscaped x) = case x of
+  String s -> B.fromText $ T.pack s
+  Text s -> B.fromText s
+  s -> fromChoiceString d s
+fromChoiceString d (External x) = case x of
+  -- Check that the sequence "</" is *not* in the external data.
+  String s -> if "</" `isInfixOf` s then mempty else B.fromText (T.pack s)
+  Text s -> if "</" `T.isInfixOf` s then mempty else B.fromText s
+  ByteString s -> if "</" `S.isInfixOf` s then mempty else B.fromText (d s)
+  s -> fromChoiceString d s
+fromChoiceString d (AppendChoiceString x y) =
+  fromChoiceString d x `mappend` fromChoiceString d y
+fromChoiceString _ EmptyChoiceString = mempty
+{-# INLINE fromChoiceString #-}
+
+modify_open :: StaticString -> Text
+modify_open open =
+  let a = getText open
+   in T.cons '<' (T.append "html:" (T.tail a))
+
+modify_key :: StaticString -> Text
+modify_key key =
+  let a = getText key
+   in T.dropEnd 2 (T.strip a)
+
+-- Escape for forester lexer
+wrap_verb :: Builder -> Builder
+wrap_verb w = B.fromLazyText $ L.foldr go "" (B.toLazyText w)
+  where
+    go :: Char -> L.Text -> L.Text
+    go '[' acc = L.append "\\startverb[\\stopverb" acc
+    go ']' acc = L.append "\\startverb]\\stopverb" acc
+    go x acc = L.cons x acc
+
+renderMarkupBuilderWith ::
+  (ByteString -> Text) ->
+  Html ->
+  Builder
+renderMarkupBuilderWith d = go mempty
+  where
+    go :: Builder -> MarkupM b -> Builder
+    go attrs (Parent _ open close content) =
+      mconcat
+        [ B.fromText "\\",
+          B.fromText (modify_open open),
+          B.fromText ">",
+          attrs,
+          B.fromText "{",
+          go mempty content,
+          B.fromText "}"
+        ]
+    go attrs (CustomParent tag content) =
+      mconcat
+        [ B.fromText "\\<html:",
+          fromChoiceString d tag,
+          B.fromText ">",
+          attrs,
+          B.fromText "{",
+          go mempty content,
+          fromChoiceString d tag,
+          B.fromText "}"
+        ]
+    go attrs (Leaf _ begin end _) =
+      mconcat
+        [ B.fromText (modify_open begin),
+          B.fromText ">",
+          attrs,
+          B.fromText "{}"
+        ]
+    go attrs (CustomLeaf tag close _) =
+      mconcat
+        [ B.fromText "\\<html:",
+          fromChoiceString d tag,
+          attrs,
+          B.fromText ">{}"
+        ]
+    go attrs (AddAttribute _ key value h) =
+      go
+        ( mconcat
+            [ B.singleton '[',
+              B.fromText (modify_key key),
+              B.fromText "]{",
+              wrap_verb (fromChoiceString d value),
+              B.fromText "}",
+              attrs
+            ]
+        )
+        h
+    go attrs (AddCustomAttribute key value h) =
+      go
+        ( mconcat
+            [ B.singleton '[',
+              fromChoiceString d key,
+              B.fromText "]{",
+              wrap_verb (fromChoiceString d value),
+              B.fromText "}",
+              attrs
+            ]
+        )
+        h
+    go _ (Content content _) = wrap_verb (fromChoiceString d content)
+    go _ (Comment comment _) = B.fromText "% " <> fromChoiceString d comment
+    go attrs (Append h1 h2) = go attrs h1 <> go attrs h2
+    go _ (Empty _) = mempty
+    {-# NOINLINE go #-}
+{-# INLINE renderMarkupBuilderWith #-}
+
+renderMarkupWith :: (ByteString -> Text) -> Html -> L.Text
+renderMarkupWith d = B.toLazyText . renderMarkupBuilderWith d
+{-# INLINE renderMarkupWith #-}
+
+renderForesterHtml :: Html -> L.Text
+renderForesterHtml = renderMarkupWith decodeUtf8
+{-# INLINE renderForesterHtml #-}
diff --git a/test/LaTeXAndHTML/Tests.hs b/test/LaTeXAndHTML/Tests.hs
@@ -147,6 +147,8 @@ mkLaTeXOrHTMLTest k copy agdaBin testDir inp =
                   then "rst"
                   else if "OrgHighlight" `List.isPrefixOf` inFileName
                   then "org"
+                  else if "TreeHighlight" `List.isPrefixOf` inFileName
+                  then "tree"
                   else "html"
 
   flags :: FilePath -> [String]

diff --git a/test/LaTeXAndHTML/succeed/.gitignore b/test/LaTeXAndHTML/succeed/.gitignore
@@ -0,0 +1,3 @@
+html/
+output/
+theme
diff --git a/test/LaTeXAndHTML/succeed/Simple.html b/test/LaTeXAndHTML/succeed/Simple.html
diff --git a/test/LaTeXAndHTML/succeed/TreeHighlightSimple.flags b/test/LaTeXAndHTML/succeed/TreeHighlightSimple.flags
@@ -0,0 +1 @@
+--html-highlight=code
diff --git a/test/LaTeXAndHTML/succeed/Simple.lagda.tree → ...ML/succeed/TreeHighlightSimple.lagda.tree b/test/LaTeXAndHTML/succeed/Simple.lagda.tree → ...ML/succeed/TreeHighlightSimple.lagda.tree
@@ -2,7 +2,7 @@
 
 \p{This is test file}
 \agda{
-module Simple where
+module TreeHighlightSimple where
 
   data Bool : Set where
             true : Bool

diff --git a/test/LaTeXAndHTML/succeed/TreeHighlightSimple.tree b/test/LaTeXAndHTML/succeed/TreeHighlightSimple.tree
@@ -0,0 +1,13 @@
+\title{simple}
+
+\p{This is test file}
+\<html:pre>[class]{Agda}{
+\<html:a>[id]{46}[class]{Keyword}{module} \<html:a>[id]{53}[href]{TreeHighlightSimple.html}[class]{Module}{TreeHighlightSimple} \<html:a>[id]{73}[class]{Keyword}{where}
+
+  \<html:a>[id]{82}[class]{Keyword}{data} \<html:a>[id]{Bool}{}\<html:a>[id]{87}[href]{TreeHighlightSimple.html#87}[class]{Datatype}{Bool} \<html:a>[id]{92}[class]{Symbol}{:} \<html:a>[id]{94}[href]{Agda.Primitive.html#388}[class]{Primitive}{Set} \<html:a>[id]{98}[class]{Keyword}{where}
+            \<html:a>[id]{Bool.true}{}\<html:a>[id]{116}[href]{TreeHighlightSimple.html#116}[class]{InductiveConstructor}{true} \<html:a>[id]{121}[class]{Symbol}{:} \<html:a>[id]{123}[href]{TreeHighlightSimple.html#87}[class]{Datatype}{Bool}
+            \<html:a>[id]{Bool.false}{}\<html:a>[id]{140}[href]{TreeHighlightSimple.html#140}[class]{InductiveConstructor}{false} \<html:a>[id]{146}[class]{Symbol}{:} \<html:a>[id]{148}[href]{TreeHighlightSimple.html#87}[class]{Datatype}{Bool}
+
+  \<html:a>[id]{a}{}\<html:a>[id]{156}[href]{TreeHighlightSimple.html#156}[class]{Function}{a} \<html:a>[id]{158}[class]{Symbol}{:} \<html:a>[id]{160}[href]{TreeHighlightSimple.html#87}[class]{Datatype}{Bool}
+  \<html:a>[id]{167}[href]{TreeHighlightSimple.html#156}[class]{Function}{a} \<html:a>[id]{169}[class]{Symbol}{=} \<html:a>[id]{171}[href]{TreeHighlightSimple.html#116}[class]{InductiveConstructor}{true}
+}
diff --git a/test/LaTeXAndHTML/succeed/TreeOneLine.html b/test/LaTeXAndHTML/succeed/TreeOneLine.html
diff --git a/test/LaTeXAndHTML/succeed/TreeOneLine.lagda.tree b/test/LaTeXAndHTML/succeed/TreeOneLine.lagda.tree
diff --git a/test/LaTeXAndHTML/succeed/forest.toml b/test/LaTeXAndHTML/succeed/forest.toml
@@ -0,0 +1,2 @@
+[forest]
+trees = ["trees", "html"]                   # The directories in which your trees are stored
diff --git a/test/LaTeXAndHTML/succeed/trees/index.tree b/test/LaTeXAndHTML/succeed/trees/index.tree
@@ -0,0 +1,3 @@
+\title{Index}
+
+\p{Check [[TreeHighlightSimple]]}
-Original file line number
+Diff line change
@@ -0,0 +1,3 @@
+    html/
+    output/
+    theme
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		[forest]
		trees = ["trees", "html"] # The directories in which your trees are stored
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,3 @@
		\title{Index}

		\p{Check [[TreeHighlightSimple]]}