diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,10 @@
# Revision history for agda2lagda
+## 0.2023.1.12
+
+* New option `--markdown` producing `.lagda.md` files instead of `.lagda.tex`.
+* Tested with GHC 8.0.2 - 9.4.4.
+
## 0.2021.6.1
* Paragraphs starting with `* ` are recognized as `\item` and
diff --git a/Makefile b/Makefile
--- a/Makefile
+++ b/Makefile
@@ -16,6 +16,9 @@
test :
cabal test
+fix-tests:
+ cabal exec -- goldplate --fix test
+
test-help:
cabal run agda2lagda -- --help
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -6,11 +6,17 @@
-agda2lagda: Convert Agda/Haskell text to literate Agda/Haskell text
-===================================================================
+agda2lagda: Convert program to literate program (Agda/Haskell)
+==============================================================
-Generate a LaTeX literate Agda/Haskell script from an Agda/Haskell script.
+Generate a literate Agda/Haskell script from an Agda/Haskell script.
+Produces LaTeX or Markdown literate scripts.
+Specification
+-------------
+
+Conversion into LaTeX (default):
+
- Single line comments are turned into ordinary LaTeX.
* Paragraphs followed by a line of equal signs are turned into `\heading`s.
* Paragraphs followed by a line of dashes are turned into `\subheading`s.
@@ -23,120 +29,92 @@
- The rest is interpreted as code and wrapped in a `code` environment.
-Examples (rendered):
-- http://www.cse.chalmers.se/~abela/#MultiSortedAlgebra
-- http://www.cse.chalmers.se/~abela/#cr-sk
-
-
-Example: `agda2lagda Foo.agda`
-
-Input: `Foo.agda`
-```agda
--- Sample non-literate Agda program
--- ================================
---
--- A remark to test bulleted lists:
---
--- * This file serves as example for agda2lagda.
---
--- * The content may be non-sensical.
---
--- Indeed!
-
-module Foo where
-
--- Some data type.
-
-data D : Set where
- c : D
-
--- A function.
-foo : D → D
-foo c = c -- basically, the identity
-
-{- This part is commented out.
-{-
-bar : D → Set
-bar x = D
--- -}
--- -}
-
--- A subheading
----------------
-
-module Submodule where
-
- postulate
- zeta : D
-
--- That's it.
--- Bye.
-```
-
-Output: `Foo.lagda.tex`
-```latex
-%% This file was automatically generated by agda2lagda 0.2021.6.1.
-
-\heading{Sample non-literate Agda program}
+Conversion into Markdown (option `--markdown`) is similar,
+but nothing needs to be done for headings and itemize environments:
-A remark to test bulleted lists:
+- Single line comments are turned into ordinary text.
+ * At the end of the file, extra block comment terminators are removed.
-\begin{itemize}
+- Comment blocks, if started on the 0th column, count as _commenting out_.
+ These will be turned into HTML comments.
+ Nested comments are not recognized.
-\item
-This file serves as example for agda2lagda.
+- The rest is interpreted as code and wrapped in a code environment (triple backticks).
-\item
-The content may be non-sensical.
+Examples
+--------
-\end{itemize}
+Given input [`Foo.agda`](https://github.com/andreasabel/agda2lagda/blob/master/test/Foo.agda):
+- Invocation `agda2lagda Foo.agda` produces output
+ [`Foo.lagda.tex`](https://github.com/andreasabel/agda2lagda/blob/master/test/golden/Foo.lagda.tex).
+- Invocation `agda2lagda --markdown Foo.agda` produces output
+ [`Foo.lagda.md`](https://github.com/andreasabel/agda2lagda/blob/master/test/golden/Foo.lagda.md).
-Indeed!
+LaTeX examples (rendered):
+- http://www.cse.chalmers.se/~abela/#MultiSortedAlgebra
+- http://www.cse.chalmers.se/~abela/#cr-sk
-\begin{code}
-module Foo where
-\end{code}
+Example `Makefile` to turn `.agda` file into highlighted HTML via Markdown (since `v0.2023.1.12`):
+```make
+FILE=Foo
+TITLE=The Title
-Some data type.
+default : md/html/$(FILE).html
-\begin{code}
-data D : Set where
- c : D
-\end{code}
+# Step 1: agda2lagda: Produce Markdown literate script.
-A function.
+md/%.lagda.md : %.agda
+ agda2lagda -f --markdown -o md/ $<
-\begin{code}
-foo : D → D
-foo c = c -- basically, the identity
-\end{code}
+# Step 2: agda: Highlight and format code blocks as HTML.
+# Also produces Agda.css.
-%% This part is commented out.
-%% {-
-%% bar : D → Set
-%% bar x = D
-%% -- -}
-%% --
+md/html/%.md : md/%.lagda.md
+ cd md ; agda --html --html-highlight=auto ../$<
-\subheading{A subheading}
+# Step 3: pandoc: Produce HTML. Improvise header to make HTML self-contained.
-\begin{code}
-module Submodule where
+md/html/%.html : md/html/%.md
+ echo '$(TITLE)' > $@
+ pandoc -f markdown -t html $< >> $@
+```
- postulate
- zeta : D
-\end{code}
+Installation from binary
+------------------------
-That's it.
-Bye.
+Binaries for Linux, macOS and Windows are available from [GitHub releases](https://github.com/andreasabel/agda2lagda/releases).
+Just download the executable for your platform there and put it in a directory that is in the system `PATH`.
+For example, under Linux (similar under macOS):
+```shell
+VERSION="0.2023.1.12"
+SRC="https://github.com/andreasabel/agda2lagda/releases/download/v${VERSION}/agda2lagda-${VERSION}-linux.binary"
+TGT="/usr/local/bin/agda2lagda"
+wget ${SRC} -O ${TGT}
+chmod +x ${TGT}
```
+For macOS, there is also a installer package, e.g.:
+```shell
+VERSION="0.2023.1.12"
+SRC="https://github.com/andreasabel/agda2lagda/releases/download/v${VERSION}/agda2lagda-${VERSION}-mac.pkg"
+TGT="/tmp/agda2lagda.pkg"
+wget ${SRC} -O ${TGT}
+open ${TGT}
+```
+Verify the installation with these commands (Linux/macOS):
+```console
+$ which agda2lagda
+/usr/local/bin/agda2lagda
+$ agda2lagda --version
+agda2lagda version 0.2023.1.12
+```
-## Installation
+Installation from source
+------------------------
These are standard installation instructions.
-Last update of installation instructions: 2021-05-29.
+Last update of installation instructions: 2023-01-11.
### From stackage.org
@@ -162,9 +140,9 @@
cabal install
```
Alternatively to the last line, you can use `stack`.
-E.g. if you have GHC 8.10.2 installed, you can use this compiler as follows:
+E.g. if you have GHC 8.10.7 installed, you can use this compiler as follows:
```
-stack install --system-ghc --stack-yaml stack-8.10.2.yaml
+stack install --system-ghc --stack-yaml stack-8.10.7.yaml
```
Alternatively, `stack` can install the compiler for you:
```
@@ -174,4 +152,4 @@
choose one (for which there is a `.yaml` file).
At the time of writing, installation with these GHC versions has been tested:
-8.0.2, 8.2.2, 8.4.4, 8.6.5, 8.8.4, 8.10.4, 9.0.1.
+8.0.2, 8.2.2, 8.4.4, 8.6.5, 8.8.4, 8.10.7, 9.0.2, 9.2.5, 9.4.4.
diff --git a/agda2lagda.cabal b/agda2lagda.cabal
--- a/agda2lagda.cabal
+++ b/agda2lagda.cabal
@@ -2,7 +2,7 @@
-- NB: Cabal file initially generated by 'cabal init'.
name: agda2lagda
-version: 0.2021.6.1
+version: 0.2023.1.12
synopsis: Translate .agda files into .lagda.tex files.
description: Simple command line tool to convert plain Agda
@@ -16,7 +16,7 @@
author: Andreas Abel
maintainer: Andreas Abel
-copyright: Andreas Abel, 2020, 2021
+copyright: Andreas Abel, 2020, 2021, 2022
category: Dependent types, Development
build-type: Simple
@@ -24,16 +24,20 @@
extra-source-files: CHANGELOG.md
README.md
Makefile
- test/Foo.agda
- test/ClosingCommentInString.agda
+ test/*.goldplate
+ test/*.agda
+ test/golden/*.lagda.md
+ test/golden/*.lagda.tex
tested-with: GHC == 8.0.2
GHC == 8.2.2
GHC == 8.4.4
GHC == 8.6.5
GHC == 8.8.4
- GHC == 8.10.4
- GHC == 9.0.1
+ GHC == 8.10.7
+ GHC == 9.0.2
+ GHC == 9.2.5
+ GHC == 9.4.4
source-repository head
type: git
@@ -42,13 +46,14 @@
source-repository this
type: git
location: git://github.com/andreasabel/agda2lagda.git
- tag: v0.2021.6.1
+ tag: v0.2023.1.12
executable agda2lagda
main-is: Main.hs
other-modules: LexicalStructure
Markup
+ Options
Render
Util
Version
@@ -94,6 +99,7 @@
-- TypeSynonymInstances
ghc-options: -Wall
+ -Wcompat
-Wno-missing-pattern-synonym-signatures
test-suite test
@@ -106,3 +112,5 @@
-- goldplate requires ghc >= 8.4
, process
build-tool-depends: goldplate:goldplate
+ -- We also need to depend on ourselves since goldplate calls us.
+ , agda2lagda:agda2lagda
diff --git a/src/Main.hs b/src/Main.hs
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -11,39 +11,23 @@
module Main where
import Control.Monad
-import qualified Data.List as List
-import Data.Semigroup
-import Options.Applicative
-import Options.Applicative.Help.Pretty (vcat, text) -- , (<$$>))
-
-import System.Directory (doesFileExist, doesDirectoryExist, createDirectoryIfMissing)
-import System.FilePath
- (splitExtension, addExtension, takeFileName, takeDirectory, hasTrailingPathSeparator, ())
+import System.Directory (doesFileExist, createDirectoryIfMissing)
+import System.FilePath (takeDirectory)
import System.IO (hPutStr, stderr)
import System.Exit (exitFailure)
import LexicalStructure
+import Options
import Render
-import Util ((<&>))
-import Version
-self :: String
-self = "agda2lagda"
-
-extensionMap :: [(String,String)]
-extensionMap =
- [ (".agda" , ".lagda.tex")
- , (".hs" , ".lhs")
- ]
-
main :: IO ()
main = do
-- Parse options.
opts@Options{..} <- options
- target <- getTarget opts
+ target@(language, format, mout) <- getTarget opts
chat opts $ vocalizeOptions opts target
-- Parse input.
@@ -53,12 +37,14 @@
-- Generate output.
- let result = lagdaTex items
+ let result = case format of
+ LaTeX -> lagdaTex items
+ Markdown -> lagdaMd language items
-- Save to file or print to stdout.
chat opts $ "Writing output...\n"
- case target of
+ case mout of
Nothing -> putStr result
Just outFile -> do
@@ -79,155 +65,6 @@
-- Done.
chat opts $ unwords [ self, "terminated successfully.\n" ]
-
--- * Option parsing and handling
-
-data Options = Options
- { optVerbose :: Bool
- , optDryRun :: Bool
- , optForce :: Bool
- , optOutput :: Maybe FilePath
- , optInput :: Maybe FilePath
- } deriving Show
-
-options :: IO Options
-options =
- execParser $
- info (helper <*> versionOption <*> numericVersionOption <*> programOptions)
- (header "Translates Agda/Haskell text into literate Agda/Haskell text, turning line comments into ordinary text and code into TeX code blocks."
- <> footerDoc (Just foot))
-
- where
- versionOption =
- infoOption (unwords versionWords)
- $ long "version"
- <> help "Show version info."
- versionWords = concat
- [ [ self, "version", version ]
- , [ "(Halloween edition)" | ".11.1" `List.isSuffixOf` version ]
- ]
-
- numericVersionOption =
- infoOption version
- $ long "numeric-version"
- <> help "Show just version number."
- -- Newline at the end:
- -- <> helpDoc (Just $ text "Show just version number." <$$> text "")
-
- programOptions = Options
- <$> oVerbose
- <*> oDryRun
- <*> oForce
- <*> oOutput
- <*> (oStdin <|> oInput)
-
- oForce =
- switch
- $ long "force"
- <> short 'f'
- <> help "Overwrite existing output files."
-
- oDryRun =
- switch
- $ long "dry-run"
- <> help "Do not write any output files, write to standard output."
-
- oVerbose =
- switch
- $ long "verbose"
- <> short 'v'
- <> help "Comment on what is happening."
-
- oOutput =
- optional $ strOption
- $ long "output"
- <> short 'o'
- <> metavar "OUT"
- <> action "directory"
- <> help "Name of output file or directory."
-
- oStdin =
- flag' Nothing
- $ long "stdin"
- <> help "Read from standard input."
-
- oInput :: Parser (Maybe FilePath)
- oInput = dashToStdin <$> do
- strArgument
- $ metavar "INFILE"
- <> action "file"
- <> help "The input file containing the Agda/Haskell text."
- where
- -- dash is interpreted as stdin
- dashToStdin = \case
- "-" -> Nothing
- file -> Just file
-
- foot = vcat $ map text $ concat
- [ [ "Unless explicitly given via -o, the name of the output file is computed by replacing the extension of the input file, according to the following rules:"
- , "" ]
- , flip map extensionMap $ \ (src, tgt) ->
- List.intercalate "\t" [ "", src, "-->", tgt ]
- , [ ""
- , "If the path OUT given via -o is a directory, that's where the output file will be placed."
- , ""
- , unwords [ "Example:", self, "path/to/file.agda" ]
- , ""
- , "This will write file path/to/file.lagda.tex unless it already exists."
- , "To overwrite existing files, use option -f."
- , ""
- , unwords [ "Example:", self, "path/to/file.hs", "-o out/dir" ]
- , ""
- , "This places the output in file out/dir/file.lhs."
- , ""
- , unwords [ "Example:", self, "path/to/file.hs", "-o new/dir/" ]
- , ""
- , "This places the output in file new/dir/file.lhs, creating directories new/ and new/dir/ if necessary."
- ]
- ]
-
-type Target = Maybe FilePath
-
-vocalizeOptions :: Options -> Target -> String
-vocalizeOptions Options{..} target = unlines $ map concat
- [ [ "Plan:" ]
- , [ "- Read from "
- , maybe "standard input" ("file " ++) optInput
- , "."
- ]
- , [ "- Write to "
- , maybe "standard output" (\ f -> "file " ++ f ++ unlessNewer) target
- , "."
- ]
- ]
- where
- unlessNewer
- | optForce = ""
- | otherwise = " (only if output is not newer than input)"
-
-getTarget :: Options -> IO Target
-getTarget Options{..}
- | optDryRun = return Nothing
- | otherwise = traverse dirOrFile optOutput <&> \ mout ->
- if | Just (File out) <- mout -> Just out
- | Just inp <- optInput ->
- case splitExtension inp of
- (base, src) | Just tgt <- lookup src extensionMap
- -> Just $ addDir mout $ addExtension base tgt
- _ -> Nothing
- | otherwise -> Nothing
- where
- addDir (Just (Dir dir)) = (dir ) . takeFileName
- addDir _ = id
-
-data DirOrFile = Dir FilePath | File FilePath
-
-dirOrFile :: FilePath -> IO DirOrFile
-dirOrFile path
- | hasTrailingPathSeparator path = return $ Dir path
- | otherwise = doesDirectoryExist path <&> \case
- True -> Dir path
- False -> File path
chat :: Options -> String -> IO ()
chat o msg = when (optVerbose o) $ hPutStr stderr msg
diff --git a/src/Markup.hs b/src/Markup.hs
--- a/src/Markup.hs
+++ b/src/Markup.hs
@@ -5,6 +5,7 @@
module Markup
( markup, Item(..), TextItem(..)
+ , gobbleTrailingBlockCommentClosers
) where
import Util
diff --git a/src/Options.hs b/src/Options.hs
new file mode 100644
--- /dev/null
+++ b/src/Options.hs
@@ -0,0 +1,243 @@
+module Options
+ ( Options(..)
+ , options
+ , Format(..)
+ , Language(..)
+ , languageToHighlighter
+ , getTarget
+ , self
+ , vocalizeOptions
+ )
+ where
+
+import qualified Data.List as List
+
+import Options.Applicative
+import Options.Applicative.Help.Pretty (vcat, text) -- , (<$$>))
+
+import System.Directory (doesDirectoryExist)
+import System.FilePath
+ (splitExtension, addExtension, takeFileName, hasTrailingPathSeparator, ())
+
+import Util
+import Version
+
+self :: String
+self = "agda2lagda"
+
+extensionMap :: [(String,(Language,[(Format,String)]))]
+extensionMap =
+ [ (".agda" , (Agda , [ (LaTeX , ".lagda.tex")
+ , (Markdown , ".lagda.md" ) ]))
+ , (".hs" , (Haskell , [ (LaTeX , ".lhs" )
+ , (Markdown , ".lhs" ) ]))
+ ]
+
+-- | Format of the output.
+data Format
+ = LaTeX -- ^ Latex literate text.
+ | Markdown -- ^ Markdown literate text.
+ deriving (Eq, Show)
+
+-- formatToLongOption :: Format -> String
+-- formatToLongOption = map toLower . show
+
+data Language
+ = Agda
+ | Haskell
+ deriving (Eq, Show)
+
+-- | Get markdown highlighter identifier (e.g. "agda", "haskell") for language.
+languageToHighlighter :: Language -> String
+languageToHighlighter = map toLower . show
+
+-- * Option parsing and handling
+
+data Options = Options
+ { optVerbose :: Bool
+ , optDryRun :: Bool
+ , optForce :: Bool
+ , optFormat :: Format
+ -- , optLatex :: Bool
+ -- , optMarkdown :: Bool
+ , optOutput :: Maybe FilePath
+ , optInput :: Maybe FilePath
+ } deriving Show
+
+options :: IO Options
+options =
+ execParser $
+ info (helper <*> versionOption <*> numericVersionOption <*> programOptions)
+ (header "Translates Agda/Haskell text into literate Agda/Haskell text, turning line comments into ordinary text and code into TeX code blocks."
+ <> footerDoc (Just foot))
+
+ where
+ versionOption =
+ infoOption (unwords versionWords)
+ $ long "version"
+ <> hidden
+ <> help "Show version info."
+ versionWords = concat
+ [ [ self, "version", version ]
+ , [ "(Halloween edition)" | ".11.1" `List.isSuffixOf` version ]
+ ]
+
+ numericVersionOption =
+ infoOption version
+ $ long "numeric-version"
+ <> hidden
+ <> help "Show just version number."
+ -- Newline at the end:
+ -- <> helpDoc (Just $ text "Show just version number." <$$> text "")
+
+ programOptions = Options
+ <$> oVerbose
+ <*> oDryRun
+ <*> oForce
+ <*> oFormat
+ <*> oOutput
+ <*> (oStdin <|> oInput)
+
+ oForce =
+ switch
+ $ long "force"
+ <> short 'f'
+ <> help "Overwrite existing output files."
+
+ oDryRun =
+ switch
+ $ long "dry-run"
+ <> hidden
+ <> help "Do not write any output files, write to standard output."
+
+ oVerbose =
+ switch
+ $ long "verbose"
+ <> short 'v'
+ <> hidden
+ <> help "Comment on what is happening."
+
+ oFormat =
+ flag LaTeX Markdown
+ $ long "markdown"
+ <> help "Produce Markdown instead of LaTeX."
+
+ -- oLaTeX =
+ -- switch
+ -- $ long (formatToLongOption LaTeX)
+ -- <> help (concat ["Generate LaTeX (default if --", formatToLongOption Markdown, " is not given)."])
+
+ -- oMarkdown =
+ -- switch
+ -- $ long (formatToLongOption Markdown)
+ -- <> help "Generate Markdown (possibly inferred from OUT file extension)."
+
+ -- oLaTeX =
+ -- optional $ strOption
+ -- $ long "latex"
+ -- <> value ""
+ -- <> noArgError (ShowHelpText Nothing)
+ -- <> metavar "LATEXFILE"
+ -- <> action "file"
+ -- <> help "Generate LaTeX (if LATEXFILE is not given, it is computed from INFILE and OUT)."
+
+ oOutput =
+ optional $ strOption
+ $ long "output"
+ <> short 'o'
+ <> metavar "OUT"
+ <> action "directory"
+ <> help "Name of output file or directory."
+
+ oStdin =
+ flag' Nothing
+ $ long "stdin"
+ <> help "Read from standard input."
+
+ oInput :: Parser (Maybe FilePath)
+ oInput = dashToStdin <$> do
+ strArgument
+ $ metavar "INFILE"
+ <> action "file"
+ <> help "The input file containing the Agda/Haskell text."
+ where
+ -- dash is interpreted as stdin
+ dashToStdin = \case
+ "-" -> Nothing
+ file -> Just file
+
+ foot = vcat $ map text $ concat
+ [ [ "Unless explicitly given via -o, the name of the output file is computed by replacing the extension of the input file, according to the following rules:"
+ , "" ]
+ , extensionMap >>= \ (src, (_language, rest)) ->
+ rest <&> \ (format, tgt) ->
+ -- let o = "--" ++ formatToLongOption format ++ ":" in
+ let o = show format in
+ List.intercalate "\t" [ "", src, "--" ++ o ++ "-->", tgt ]
+ , [ ""
+ , "If the path OUT given via -o is a directory, that's where the output file will be placed."
+ , ""
+ , unwords [ "Example:", self, "path/to/file.agda" ]
+ , ""
+ , "This will write file path/to/file.lagda.tex unless it already exists."
+ , "To overwrite existing files, use option -f."
+ , ""
+ , unwords [ "Example:", self, "path/to/file.hs", "-o out/dir" ]
+ , ""
+ , "This places the output in file out/dir/file.lhs."
+ , ""
+ , unwords [ "Example:", self, "path/to/file.hs", "-o new/dir/" ]
+ , ""
+ , "This places the output in file new/dir/file.lhs, creating directories new/ and new/dir/ if necessary."
+ ]
+ ]
+
+type Target = (Language, Format, Maybe FilePath)
+
+vocalizeOptions :: Options -> Target -> String
+vocalizeOptions Options{..} (language, format, target) = unlines $ map concat
+ [ [ "Plan:" ]
+ , [ "- Read " ++ show language ++ " code from "
+ , maybe "standard input" ("file " ++) optInput
+ , "."
+ ]
+ , [ "- Write " ++ show format ++ " to "
+ , maybe "standard output" (\ f -> "file " ++ f ++ unlessNewer) target
+ , "."
+ ]
+ ]
+ where
+ unlessNewer
+ | optForce = ""
+ | otherwise = " (only if output is not newer than input)"
+
+getTarget :: Options -> IO Target
+getTarget Options{..} = do
+ let language = maybe Agda fst m
+ outFile <- if optDryRun then return Nothing else do
+ traverse dirOrFile optOutput <&> \ mout ->
+ if | Just (File out) <- mout -> Just out
+ | Just (_, (base, tgt)) <- m -> Just $ addDir mout $ addExtension base tgt
+ | otherwise -> Nothing
+ return (language, optFormat, outFile)
+ where
+ -- Resolve Language, basename, and extension from input file.
+ m :: Maybe (Language, (FilePath, FilePath))
+ m = do
+ inp <- optInput
+ let (base, src) = splitExtension inp
+ (language, rest) <- lookup src extensionMap
+ ext <- lookup optFormat rest
+ Just (language, (base, ext))
+
+ addDir (Just (Dir dir)) = (dir ) . takeFileName
+ addDir _ = id
+
+data DirOrFile = Dir FilePath | File FilePath
+
+dirOrFile :: FilePath -> IO DirOrFile
+dirOrFile path
+ | hasTrailingPathSeparator path = return $ Dir path
+ | otherwise = doesDirectoryExist path <&> \case
+ True -> Dir path
+ False -> File path
diff --git a/src/Render.hs b/src/Render.hs
--- a/src/Render.hs
+++ b/src/Render.hs
@@ -5,11 +5,11 @@
module Render
( lagdaTex
+ , lagdaMd
) where
-import Util
-
import qualified LexicalStructure as L
+import Options (Language, languageToHighlighter)
import Markup
import Version
@@ -43,3 +43,21 @@
, map (unlines . ("\\item" :)) ps
, [ "\\end{itemize}" ]
]
+
+-- | Render into literate Markdown Agda.
+
+lagdaMd :: Language -> [L.Item] -> String
+lagdaMd language its = unlines $ concat
+ [ [""]
+ , [""]
+ , map render $ gobbleTrailingBlockCommentClosers its
+ ]
+ where
+ render = \case
+ L.TextItem s -> s
+ L.CommItem s -> unwords [""]
+ L.CodeItem s -> concat
+ [ "```" ++ languageToHighlighter language ++ "\n"
+ , s
+ , "```\n"
+ ]
diff --git a/src/Util.hs b/src/Util.hs
--- a/src/Util.hs
+++ b/src/Util.hs
@@ -3,10 +3,11 @@
module Util (module Util, module X) where
import Data.Bifunctor as X
-import Data.Char as X (isSpace)
+import Data.Char as X (isSpace, toLower)
import Data.Function as X (on)
import Data.List as X (dropWhileEnd, groupBy)
import Data.Maybe as X
+import Data.Semigroup as X
(<&>) :: Functor f => f a -> (a -> b) -> f b
(<&>) = flip (<$>)
diff --git a/test/golden/ClosingCommentInString.lagda.md b/test/golden/ClosingCommentInString.lagda.md
new file mode 100644
--- /dev/null
+++ b/test/golden/ClosingCommentInString.lagda.md
@@ -0,0 +1,40 @@
+
+
+This demonstrates a known issue:
+The parser is not aware of strings, thus,
+a closing block comment delimiter inside a string
+is taken as a closing block comment delimiter.
+
+Without nested comments:
+
+
+```agda
+ and other garbage @#$% that appears now as Agda code!"
+-}
+```
+
+With nested comments:
+
+
+```agda
+This should be still commented-out. -}
+```
+
+The reverse situation:
+
+```agda
+test = "Never put comment opening {- inside a string!"
+
+postulate
+ ThisShouldNotBeCommentedOut : Set
+
+-- -} This should be text, not code!!
+```
+
+SNAFU.
diff --git a/test/golden/ClosingCommentInString.lagda.tex b/test/golden/ClosingCommentInString.lagda.tex
new file mode 100644
--- /dev/null
+++ b/test/golden/ClosingCommentInString.lagda.tex
@@ -0,0 +1,41 @@
+%% This file was automatically generated by agda2lagda 0.2023.1.12.
+
+This demonstrates a known issue:
+The parser is not aware of strings, thus,
+a closing block comment delimiter inside a string
+is taken as a closing block comment delimiter.
+
+Without nested comments:
+
+%% This is commented-out.
+%% test = "A weird string with comment closing
+
+\begin{code}
+ and other garbage @#$% that appears now as Agda code!"
+-}
+\end{code}
+
+With nested comments:
+
+%%
+%% {- This is commented-out.
+%% test = "A weird string with comment closing -} and other garbage @#$%!"
+%% -- NB: this confuses even Agda (at the time of writing, version 2.6.1).
+
+\begin{code}
+This should be still commented-out. -}
+\end{code}
+
+The reverse situation:
+
+\begin{code}
+test = "Never put comment opening {- inside a string!"
+
+postulate
+ ThisShouldNotBeCommentedOut : Set
+
+-- -} This should be text, not code!!
+\end{code}
+
+SNAFU.
+
diff --git a/test/golden/Foo.lagda.md b/test/golden/Foo.lagda.md
new file mode 100644
--- /dev/null
+++ b/test/golden/Foo.lagda.md
@@ -0,0 +1,50 @@
+
+
+Sample non-literate Agda program
+================================
+
+A remark to test bulleted lists:
+
+* This file serves as example for agda2lagda.
+
+* The content may be non-sensical.
+
+Indeed!
+
+```agda
+module Foo where
+```
+
+Some data type.
+
+```agda
+data D : Set where
+ c : D
+```
+
+A function.
+
+```agda
+foo : D → D
+foo c = c -- basically, the identity
+```
+
+
+A subheading
+-------------
+
+```agda
+module Submodule where
+
+ postulate
+ zeta : D
+```
+
+That's it.
+Bye.
diff --git a/test/golden/Foo.lagda.tex b/test/golden/Foo.lagda.tex
new file mode 100644
--- /dev/null
+++ b/test/golden/Foo.lagda.tex
@@ -0,0 +1,55 @@
+%% This file was automatically generated by agda2lagda 0.2023.1.12.
+
+\heading{Sample non-literate Agda program}
+
+A remark to test bulleted lists:
+
+\begin{itemize}
+
+\item
+This file serves as example for agda2lagda.
+
+\item
+The content may be non-sensical.
+
+\end{itemize}
+
+Indeed!
+
+\begin{code}
+module Foo where
+\end{code}
+
+Some data type.
+
+\begin{code}
+data D : Set where
+ c : D
+\end{code}
+
+A function.
+
+\begin{code}
+foo : D → D
+foo c = c -- basically, the identity
+\end{code}
+
+%% This part is commented out.
+%% {-
+%% bar : D → Set
+%% bar x = D
+%% -- -}
+%% --
+
+\subheading{A subheading}
+
+\begin{code}
+module Submodule where
+
+ postulate
+ zeta : D
+\end{code}
+
+That's it.
+Bye.
+
diff --git a/test/markdown.goldplate b/test/markdown.goldplate
new file mode 100644
--- /dev/null
+++ b/test/markdown.goldplate
@@ -0,0 +1,9 @@
+{
+ "command": "agda2lagda",
+ "input_files": "*.agda",
+ "arguments": ["--dry-run", "--markdown", "${GOLDPLATE_INPUT_FILE}"],
+ "asserts": [
+ {"exit_code": 0},
+ {"stdout": "golden/${GOLDPLATE_INPUT_NAME}.lagda.md"}
+ ]
+}
diff --git a/test/tests.goldplate b/test/tests.goldplate
new file mode 100644
--- /dev/null
+++ b/test/tests.goldplate
@@ -0,0 +1,9 @@
+{
+ "command": "agda2lagda",
+ "input_files": "*.agda",
+ "arguments": ["--dry-run", "${GOLDPLATE_INPUT_FILE}"],
+ "asserts": [
+ {"exit_code": 0},
+ {"stdout": "golden/${GOLDPLATE_INPUT_NAME}.lagda.tex"}
+ ]
+}