Allow using Pandoc filter in LaTeX commands

.github/workflows/ci-ubuntu.yml

@@ -24,9 +24,9 @@ on:
 ########################################################################
 
 env:
-  IDRIS2_COMMIT: 9e84b153bd3d7d5a63ec9e6a9adfa47a067ea172
+  IDRIS2_COMMIT: e4431891e915c6866a6eea18046dcb3bcdfa8d89
   COLLIE_COMMIT: ed2eda5e04fbd02a7728e915d396e14cc7ec298e
-  IDRALL_COMMIT: 62a455894b1db5134c8b56d31aadb31d483a4b2c
+  IDRALL_COMMIT: 86d84e44f7e2d07e597ca10b7d0a3451992b5605
   SCHEME: scheme
 
 ########################################################################
@@ -61,6 +61,7 @@ jobs:
           sudo apt-get update
           sudo apt-get install -y chezscheme
           sudo apt-get install -y texlive texlive-fonts-extra
+          sudo apt-get install -y pandoc
 
       - name: Install Idris2 & its API
         if: steps.cache-idris2.outputs.cache-hit != 'true'

Makefile

@@ -1,13 +1,13 @@
 .PHONY: project src install test doc clean
 
-project: build/exec/katla
+project: build/exec/katla build/exec/katla-pandoc
 
 src: src/**/*.idr
 
 build/exec/katla: src 
 	idris2 --build katla.ipkg
 
-build/exec/katla-pandoc: .PHONY
+build/exec/katla-pandoc:
 	idris2 --build katla-pandoc.ipkg
 
 install: build/exec/katla build/exec/katla-pandoc

src/Katla/Pandoc.idr

@@ -161,36 +161,39 @@ checkCode dir packages snippets = do
             | (msg, err) => die $ "Error checking Idris code (exit code: \{show err})\n" ++ msg
         pure ()
 
+addPandocHeaderIncludes : List String -> JSON -> JSON
+addPandocHeaderIncludes newHeaders doc = do
+    let newHeaders = map (\newHeader => JObject [
+            ("t", JString "MetaBlocks"),
+            ("c", JArray [JObject [
+                ("t", JString "RawBlock"),
+                ("c", JArray [JString "tex", JString newHeader])
+            ]])
+        ]) newHeaders
+    update (Just . update (Just . update (Just . (\case
+        JArray existingHeaders => JArray $ existingHeaders ++ newHeaders
+        existingHeader => JArray $ existingHeader :: newHeaders) .
+        maybe (JArray []) id) "c" .
+        maybe (JObject [("t", JString "MetaList")]) id) "header-includes" .
+        maybe (JObject []) id) "meta" doc
+
 covering
 addKatlaHeader : JSON -> IO JSON
 addKatlaHeader doc = do
     (katlaHeader, 0) <- run "katla latex preamble"
         | (_, err) => die "Error getting Katla header (exit code: \{show err})"
 
-    let pandocKatlaHeader = JObject [
-        ("t", JString "MetaBlocks"),
-        ("c", JArray [JObject [
-            ("t", JString "RawBlock"),
-            ("c", JArray [JString "tex", JString katlaHeader])
-        ]])
-    ]
-
-    pure $ update (Just . update (Just . update (Just . (\case
-          JArray xs => JArray $ pandocKatlaHeader :: xs
-          json => json) .
-          maybe (JArray []) id) "c" .
-          maybe (JObject [("t", JString "MetaList")]) id) "header-includes" .
-          maybe (JObject []) id) "meta" doc
+    pure $ addPandocHeaderIncludes [katlaHeader] doc
 
 covering
-formatSnippet : (dir : String) -> Snippet -> (start : Nat) -> (len : Nat) -> IO JSON
-formatSnippet dir snippet start len = do
+formatSnippet : (dir : String) -> Snippet -> (snippetName : String) -> (start : Nat) -> (len : Nat) -> IO (Maybe String, JSON)
+formatSnippet dir snippet snippetName start len = do
     let False = snippet.hide
-        | True => pure $ JObject [("t", JString "Para"), ("c", JArray [])]
+        | True => pure (Nothing, JObject [("t", JString "Para"), ("c", JArray [])])
 
     let katlaCmd = case snippet.displayType of
-          Block => "katla latex macro KatlaSnippet \{dir}/\{snippet.file}.idr build/ttc/*/\{dir}/\{snippet.file}.ttm \{show start} 0 \{show len}"
-          Inline => "katla latex macro inline KatlaSnippet \{dir}/\{snippet.file}.idr build/ttc/*/\{dir}/\{snippet.file}.ttm \{show start} 0 \{show $ 1 + len} \{show $ 8 + length snippet.code}"
+          Block => "katla latex macro \{snippetName} \{dir}/\{snippet.file}.idr build/ttc/*/\{dir}/\{snippet.file}.ttm \{show start} 0 \{show len}"
+          Inline => "katla latex macro inline \{snippetName} \{dir}/\{snippet.file}.idr build/ttc/*/\{dir}/\{snippet.file}.ttm \{show start} 0 \{show $ 1 + len} \{show $ 8 + length snippet.code}"
     (out, 0) <- run katlaCmd
         | (_, err) => die "Error running Katla (exit code: \{show err})"
 
@@ -199,13 +202,10 @@ formatSnippet dir snippet start len = do
           Decls => out
           Expr _ => dedent out
 
-    pure $ JObject [
+    pure (Just out, JObject [
         ("t", JString $ case snippet.displayType of Block => "RawBlock"; Inline => "RawInline"),
-        ("c", JArray [
-            JString "tex",
-            JString $ "\\let\\KatlaSnippet\\relax{}" ++ out ++ "\\KatlaSnippet{}"
-        ])
-    ]
+        ("c", JArray [ JString "tex", JString "\\\{snippetName}{}"])
+    ])
   where
     katlaIndent : String
     katlaIndent = "\\KatlaSpace{}\\KatlaSpace{}\\KatlaSpace{}\\KatlaSpace{}"
@@ -223,13 +223,31 @@ formatSnippet dir snippet start len = do
 
 covering
 addKatlaSnippets : (dir : String) -> List Snippet -> List (Nat, Nat) -> JSON -> IO JSON
-addKatlaSnippets dir snippets ranges json = do
-    evalStateT ranges $ traverseSnippets (\snippet => do
-        Just (start, len) <- gets head'
-            | Nothing => die "katla-pandoc internal error"
-        modify (\case [] => []; _ :: xs => xs)
-        lift $ formatSnippet dir snippet start len
-      ) json
+addKatlaSnippets dir snippets ranges doc = do
+    ((headers, _), doc) <- runStateT (the (SnocList String) [<], ranges) $ traverseSnippets (\snippet => do
+        (headers, (start, len) :: rest) <- get {stateType = (SnocList String, List (Nat, Nat))}
+            | _ => die "katla-pandoc internal error"
+
+        snippetName <- lift genName
+        (newHeader, json) <- lift $ formatSnippet dir snippet snippetName start len
+
+        put (
+            case newHeader of Nothing => headers; Just newHeader => headers :< newHeader,
+            rest
+          )
+
+        pure json
+      ) doc
+
+    pure $ addPandocHeaderIncludes (cast headers) doc
+  where
+    alpha : List Char
+    alpha = unpack "ABCDEFGHIJKLMNOPQRSTUVWXYZ"
+
+    genName : IO String
+    genName = do
+        suffix <- for (replicate 6 ()) $ \() => rndSelect alpha
+        pure "KatlaSnippet\{pack suffix}"
 
 covering
 main : IO ()

tests/examples/pandoc/Source.md

@@ -24,6 +24,31 @@ x : Nat
 x = 1 + 2
 ```
 
+And here's a code block in a \LaTeX{} figure environment:
+
+```{=latex}
+\newcommand\myfig[2]{
+    \begin{figure}[h]
+    \centering
+    #2
+    \caption{#1}
+    \end{figure}
+}
+```
+
+```{=latex}
+\myfig{Definition of $y$}{
+```
+
+```idr
+y : Nat
+y = x + 3
+```
+
+```{=latex}
+}
+```
+
 We can use namespaces by adding the `namespace` attribute, such as to provide alternate definitions for functions. Consider this function signature:
 
 ```{.idr namespace="A"}

tests/examples/pandoc/run

@@ -1,8 +1,10 @@
+PATH="../../../build/exec:$PATH"
+
 rm -rf temp build
 
 mkdir temp
 
 # Test Katla pandoc
-pandoc ./Source.md --filter "$1-pandoc" -o temp/source.tex
+pandoc ./Source.md --filter "$1-pandoc" --to=latex | sed 's/KatlaSnippet[[:alpha:]]\+/KatlaSnippet/g' > temp/source.tex
 pandoc ./Source.md --filter "$1-pandoc" -o temp/source.pdf
 diff source-expected.tex temp/source.tex >> output

tests/examples/pandoc/source-expected.tex

@@ -15,132 +15,74 @@ \section{Basic Usage}\label{basic-usage}}
 
 We can use all Idris 2 features. Here's an example code block:
 
-\let\KatlaSnippet\relax{}\newcommand\KatlaSnippet[1][]{\UseVerbatim[#1]{KatlaSnippet}}
-\begin{SaveVerbatim}[commandchars=\\\{\}]{KatlaSnippet}
-\IdrisFunction{x}\KatlaSpace{}\IdrisKeyword{:}\KatlaSpace{}\IdrisType{Nat}\KatlaNewline{}
-\IdrisFunction{x}\KatlaSpace{}\IdrisKeyword{=}\KatlaSpace{}\IdrisData{1}\KatlaSpace{}\IdrisFunction{+}\KatlaSpace{}\IdrisData{2}\KatlaNewline{}
-\end{SaveVerbatim}
 \KatlaSnippet{}
 
+And here's a code block in a \LaTeX{} figure environment:
+
+\newcommand\myfig[2]{
+    \begin{figure}[h]
+    \centering
+    #2
+    \caption{#1}
+    \end{figure}
+}
+
+\myfig{Definition of $y$}{
+
+\KatlaSnippet{}
+
+}
+
 We can use namespaces by adding the \texttt{namespace} attribute, such
 as to provide alternate definitions for functions. Consider this
 function signature:
 
-\let\KatlaSnippet\relax{}\newcommand\KatlaSnippet[1][]{\UseVerbatim[#1]{KatlaSnippet}}
-\begin{SaveVerbatim}[commandchars=\\\{\}]{KatlaSnippet}
-\IdrisFunction{f}\KatlaSpace{}\IdrisKeyword{:}\KatlaSpace{}\IdrisType{Vect}\KatlaSpace{}\IdrisBound{n}\KatlaSpace{}\IdrisBound{a}\KatlaSpace{}\IdrisKeyword{\KatlaDash{}>}\KatlaSpace{}\IdrisType{Vect}\KatlaSpace{}\IdrisKeyword{(}\IdrisBound{n}\KatlaSpace{}\IdrisFunction{+}\KatlaSpace{}\IdrisBound{n}\IdrisKeyword{)}\KatlaSpace{}\IdrisBound{a}\KatlaNewline{}
-\end{SaveVerbatim}
 \KatlaSnippet{}
 
-Here's one implementation for
-\let\KatlaSnippet\relax{}\newcommand\KatlaSnippet[1][]{\UseVerb[#1]{KatlaSnippet}}
-\begin{SaveVerbatim}[commandchars=\\\{\}]{KatlaSnippet}
-\IdrisFunction{f}\KatlaNewline{}
-\end{SaveVerbatim}
-\KatlaSnippet{}:
-
-\let\KatlaSnippet\relax{}\newcommand\KatlaSnippet[1][]{\UseVerbatim[#1]{KatlaSnippet}}
-\begin{SaveVerbatim}[commandchars=\\\{\}]{KatlaSnippet}
-\IdrisFunction{f}\KatlaSpace{}\IdrisBound{xs}\KatlaSpace{}\IdrisKeyword{=}\KatlaSpace{}\IdrisBound{xs}\KatlaSpace{}\IdrisFunction{++}\KatlaSpace{}\IdrisBound{xs}\KatlaNewline{}
-\end{SaveVerbatim}
+Here's one implementation for \KatlaSnippet{}:
+
 \KatlaSnippet{}
 
 By repeating the signature in a different namespace, in a hidden code
 block, I can give an alternate definition:
 
-\let\KatlaSnippet\relax{}\newcommand\KatlaSnippet[1][]{\UseVerbatim[#1]{KatlaSnippet}}
-\begin{SaveVerbatim}[commandchars=\\\{\}]{KatlaSnippet}
-\IdrisFunction{f}\KatlaSpace{}\IdrisBound{xs}\KatlaSpace{}\IdrisKeyword{=}\KatlaSpace{}\IdrisBound{xs}\KatlaSpace{}\IdrisFunction{++}\KatlaSpace{}\IdrisFunction{reverse}\KatlaSpace{}\IdrisBound{xs}\KatlaNewline{}
-\end{SaveVerbatim}
 \KatlaSnippet{}
 
 \hypertarget{inline-code}{%
 \section{Inline Code}\label{inline-code}}
 
 As well as block code, we can have inline code, like
-\let\KatlaSnippet\relax{}\newcommand\KatlaSnippet[1][]{\UseVerb[#1]{KatlaSnippet}}
-\begin{SaveVerbatim}[commandchars=\\\{\}]{KatlaSnippet}
-\IdrisFunction{the}\KatlaSpace{}\IdrisType{Nat}\KatlaSpace{}\IdrisData{3}\KatlaNewline{}
-\end{SaveVerbatim}
-\KatlaSnippet{}. Here's another:
-\let\KatlaSnippet\relax{}\newcommand\KatlaSnippet[1][]{\UseVerb[#1]{KatlaSnippet}}
-\begin{SaveVerbatim}[commandchars=\\\{\}]{KatlaSnippet}
-\IdrisData{1}\KatlaSpace{}\IdrisFunction{+}\KatlaSpace{}\IdrisData{2}\KatlaNewline{}
-\end{SaveVerbatim}
-\KatlaSnippet{}. We can also call the function we previously defined:
-\let\KatlaSnippet\relax{}\newcommand\KatlaSnippet[1][]{\UseVerb[#1]{KatlaSnippet}}
-\begin{SaveVerbatim}[commandchars=\\\{\}]{KatlaSnippet}
-\IdrisFunction{f}\KatlaSpace{}\IdrisData{[1,}\KatlaSpace{}\IdrisData{2,}\KatlaSpace{}\IdrisData{3]}\KatlaNewline{}
-\end{SaveVerbatim}
-\KatlaSnippet{}.
+\KatlaSnippet{}. Here's another: \KatlaSnippet{}. We can
+also call the function we previously defined: \KatlaSnippet{}.
 
 By default, a code block is interpreted as top-level Idris 2
 declarations, while inline code is interpreted as an expression. But we
 can switch it up if we wish.
 
 By using the \texttt{decls} class, we can write an inline declaration:
-\let\KatlaSnippet\relax{}\newcommand\KatlaSnippet[1][]{\UseVerb[#1]{KatlaSnippet}}
-\begin{SaveVerbatim}[commandchars=\\\{\}]{KatlaSnippet}
-\IdrisFunction{g}\KatlaSpace{}\IdrisKeyword{:}\KatlaSpace{}\IdrisType{Nat}\KatlaSpace{}\IdrisKeyword{\KatlaDash{}>}\KatlaSpace{}\IdrisType{Nat}\KatlaNewline{}
-\end{SaveVerbatim}
 \KatlaSnippet{}.
 
 By using the \texttt{expr} class, we can write a block expression:
 
-\let\KatlaSnippet\relax{}\newcommand\KatlaSnippet[1][]{\UseVerbatim[#1]{KatlaSnippet}}
-\begin{SaveVerbatim}[commandchars=\\\{\}]{KatlaSnippet}
-\IdrisData{[}\KatlaNewline{}
-\KatlaSpace{}\KatlaSpace{}\KatlaSpace{}\KatlaSpace{}\IdrisData{1,}\KatlaNewline{}
-\KatlaSpace{}\KatlaSpace{}\KatlaSpace{}\KatlaSpace{}\IdrisData{2,}\KatlaNewline{}
-\KatlaSpace{}\KatlaSpace{}\KatlaSpace{}\KatlaSpace{}\IdrisData{3}\KatlaNewline{}
-\IdrisData{]}\KatlaNewline{}
-\end{SaveVerbatim}
 \KatlaSnippet{}
 
 \hypertarget{types}{%
 \section{Types}\label{types}}
 
 Sometimes, Idris 2 cannot infer the type of an expression. Is
-\let\KatlaSnippet\relax{}\newcommand\KatlaSnippet[1][]{\UseVerb[#1]{KatlaSnippet}}
-\begin{SaveVerbatim}[commandchars=\\\{\}]{KatlaSnippet}
-\IdrisData{[1,}\KatlaSpace{}\IdrisData{2,}\KatlaSpace{}\IdrisData{3]}\KatlaNewline{}
-\end{SaveVerbatim}
-\KatlaSnippet{} a
-\let\KatlaSnippet\relax{}\newcommand\KatlaSnippet[1][]{\UseVerb[#1]{KatlaSnippet}}
-\begin{SaveVerbatim}[commandchars=\\\{\}]{KatlaSnippet}
-\IdrisType{List}\KatlaSpace{}\IdrisType{Nat}\KatlaNewline{}
-\end{SaveVerbatim}
-\KatlaSnippet{}, or a
-\let\KatlaSnippet\relax{}\newcommand\KatlaSnippet[1][]{\UseVerb[#1]{KatlaSnippet}}
-\begin{SaveVerbatim}[commandchars=\\\{\}]{KatlaSnippet}
-\IdrisType{Vect}\KatlaSpace{}\IdrisData{3}\KatlaSpace{}\IdrisType{Integer}\KatlaNewline{}
-\end{SaveVerbatim}
-\KatlaSnippet{}? We can use the \texttt{type} attribute to tell Idris 2
-which one it should be.
+\KatlaSnippet{} a \KatlaSnippet{}, or a
+\KatlaSnippet{}? We can use the \texttt{type} attribute to tell
+Idris 2 which one it should be.
 
 \hypertarget{multiple-files}{%
 \section{Multiple Files}\label{multiple-files}}
 
 If you need an import to \emph{not} be available, namespaces are not
 enough. We can use the \texttt{file} attribute to put snippets in
-separate files. For example, the signature of
-\let\KatlaSnippet\relax{}\newcommand\KatlaSnippet[1][]{\UseVerb[#1]{KatlaSnippet}}
-\begin{SaveVerbatim}[commandchars=\\\{\}]{KatlaSnippet}
-\IdrisFunction{f}\KatlaNewline{}
-\end{SaveVerbatim}
-\KatlaSnippet{} fails to compile if we use a new file, that hasn't
-imported
-\let\KatlaSnippet\relax{}\newcommand\KatlaSnippet[1][]{\UseVerb[#1]{KatlaSnippet}}
-\begin{SaveVerbatim}[commandchars=\\\{\}]{KatlaSnippet}
-\IdrisType{Vect}\KatlaNewline{}
-\end{SaveVerbatim}
+separate files. For example, the signature of \KatlaSnippet{}
+fails to compile if we use a new file, that hasn't imported
 \KatlaSnippet{}.
 
-\let\KatlaSnippet\relax{}\newcommand\KatlaSnippet[1][]{\UseVerbatim[#1]{KatlaSnippet}}
-\begin{SaveVerbatim}[commandchars=\\\{\}]{KatlaSnippet}
-\IdrisKeyword{failing}\KatlaSpace{}\IdrisData{"Undefined\KatlaSpace{}name\KatlaSpace{}Vect."}\KatlaNewline{}
-\KatlaSpace{}\KatlaSpace{}\KatlaSpace{}\KatlaSpace{}\IdrisFunction{f}\KatlaSpace{}\IdrisKeyword{:}\KatlaSpace{}Vect\KatlaSpace{}n\KatlaSpace{}a\KatlaSpace{}\IdrisKeyword{\KatlaDash{}>}\KatlaSpace{}Vect\KatlaSpace{}\IdrisKeyword{(}n\KatlaSpace{}+\KatlaSpace{}n\IdrisKeyword{)}\KatlaSpace{}a\KatlaNewline{}
-\end{SaveVerbatim}
 \KatlaSnippet{}
 
 \hypertarget{packages}{%
@@ -150,11 +92,4 @@ \section{Packages}\label{packages}}
 using the \texttt{idris2-packages} key. For example, adding
 \texttt{contrib} allows us to use the \texttt{Language.JSON} module.
 
-\let\KatlaSnippet\relax{}\newcommand\KatlaSnippet[1][]{\UseVerbatim[#1]{KatlaSnippet}}
-\begin{SaveVerbatim}[commandchars=\\\{\}]{KatlaSnippet}
-\IdrisKeyword{import}\KatlaSpace{}\IdrisModule{Language.JSON}\KatlaNewline{}
-\KatlaNewline{}
-\IdrisFunction{x}\KatlaSpace{}\IdrisKeyword{:}\KatlaSpace{}\IdrisType{Maybe}\KatlaSpace{}\IdrisType{JSON}\KatlaNewline{}
-\IdrisFunction{x}\KatlaSpace{}\IdrisKeyword{=}\KatlaSpace{}\IdrisFunction{parse}\KatlaSpace{}\IdrisData{\#"\{"x":\KatlaSpace{}1,\KatlaSpace{}"y":\KatlaSpace{}2\}"\#}\KatlaNewline{}
-\end{SaveVerbatim}
 \KatlaSnippet{}