diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml index 71253ca..2ca64d6 100644 --- a/.github/workflows/ci-ubuntu.yml +++ b/.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' diff --git a/Makefile b/Makefile index 44f1945..09cb20d 100644 --- a/Makefile +++ b/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 diff --git a/src/Katla/Pandoc.idr b/src/Katla/Pandoc.idr index eb955e4..01103fb 100644 --- a/src/Katla/Pandoc.idr +++ b/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 () diff --git a/tests/examples/pandoc/Source.md b/tests/examples/pandoc/Source.md index 487879c..a355611 100644 --- a/tests/examples/pandoc/Source.md +++ b/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"} diff --git a/tests/examples/pandoc/run b/tests/examples/pandoc/run index f762eba..46afe82 100644 --- a/tests/examples/pandoc/run +++ b/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 diff --git a/tests/examples/pandoc/source-expected.tex b/tests/examples/pandoc/source-expected.tex index c0021a9..91eb51d 100644 --- a/tests/examples/pandoc/source-expected.tex +++ b/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{}