From 845f78d0930d899c67ed29d4367d614dc5610a6d Mon Sep 17 00:00:00 2001 From: Robert Wright Date: Wed, 10 Jul 2024 16:07:25 +0100 Subject: [PATCH] Add Pandoc mode --- CONTRIBUTORS | 1 + Makefile | 6 +- katla-pandoc.ipkg | 13 ++ src/Katla/Pandoc.idr | 253 ++++++++++++++++++++++ tests/Main.idr | 1 + tests/examples/pandoc/Source.md | 89 ++++++++ tests/examples/pandoc/expected | 0 tests/examples/pandoc/run | 8 + tests/examples/pandoc/source-expected.tex | 160 ++++++++++++++ 9 files changed, 530 insertions(+), 1 deletion(-) create mode 100644 katla-pandoc.ipkg create mode 100644 src/Katla/Pandoc.idr create mode 100644 tests/examples/pandoc/Source.md create mode 100644 tests/examples/pandoc/expected create mode 100644 tests/examples/pandoc/run create mode 100644 tests/examples/pandoc/source-expected.tex diff --git a/CONTRIBUTORS b/CONTRIBUTORS index c99d8d2..47d408a 100644 --- a/CONTRIBUTORS +++ b/CONTRIBUTORS @@ -1,3 +1,4 @@ Ohad Kammar Guillaume Allais Jan de Muijnck-Hughes +Robert Wright diff --git a/Makefile b/Makefile index 39a0fa7..18ebd60 100644 --- a/Makefile +++ b/Makefile @@ -5,8 +5,12 @@ project:build/exec/katla build/exec/katla: .PHONY idris2 --build katla.ipkg -install: build/exec/katla +build/exec/katla-pandoc: .PHONY + idris2 --build katla-pandoc.ipkg + +install: build/exec/katla build/exec/katla-pandoc idris2 --install katla.ipkg + idris2 --install katla-pandoc.ipkg cp -R build/exec/* ~/.idris2/bin/ test: .PHONY diff --git a/katla-pandoc.ipkg b/katla-pandoc.ipkg new file mode 100644 index 0000000..d3dabb4 --- /dev/null +++ b/katla-pandoc.ipkg @@ -0,0 +1,13 @@ +package katla-pandoc + +authors = "Robert Wright" + +depends = contrib + +modules + = Katla.Pandoc + +main = Katla.Pandoc + +executable = katla-pandoc +sourcedir = "src" diff --git a/src/Katla/Pandoc.idr b/src/Katla/Pandoc.idr new file mode 100644 index 0000000..eb955e4 --- /dev/null +++ b/src/Katla/Pandoc.idr @@ -0,0 +1,253 @@ +module Katla.Pandoc + +import Control.Monad.State + +import Data.SortedMap +import Data.SortedSet +import Data.String + +import Language.JSON +import System +import System.Directory +import System.Random + +%default total + +updateJSON : String -> (JSON -> JSON) -> JSON -> JSON +updateJSON key f json = update (\case Nothing => Just (f JNull); Just x => Just (f x)) key json + +findAttr : (key : String) -> + (default_ : String) -> + List JSON -> + String +findAttr key default_ [] = default_ +findAttr key default_ (JArray [JString k, JString v] :: attrs) = + if k == key + then v + else findAttr key default_ attrs +findAttr key default_ (_ :: attrs) = findAttr key default_ attrs + +findPackages : JSON -> List String +findPackages doc = do + let Just (JArray packages) = lookup "meta" doc >>= lookup "idris2-packages" >>= lookup "c" + | _ => [] + JObject [("t", JString "MetaInlines"), ("c", JArray [JObject [("t", JString "Str"), ("c", JString package)]])] <- packages + | _ => [] + pure package + +data DisplayType = Block | Inline + +data CodeType = Decls | Expr String + +record Snippet where + constructor MkSnippet + code : String + displayType : DisplayType + codeType : CodeType + hide : Bool + file : String + namespace_ : String + +parseSnippet : JSON -> Maybe Snippet +parseSnippet (JObject [ + ("t", JString t), + ("c", JArray [JArray [_, JArray (JString "idr" :: clss), JArray attrs], JString code]) + ]) = do + displayType <- case t of + "CodeBlock" => pure Block + "Code" => pure Inline + _ => Nothing + + let codeType = do + let exprType = findAttr "type" "?" attrs + if elem (JString "decls") clss || elem (JString "decl") clss + then Decls + else if elem (JString "expr") clss || exprType /= "?" + then Expr exprType + else case displayType of + Block => Decls + Inline => Expr exprType + + pure $ MkSnippet + code + displayType + codeType + (elem (JString "hide") clss) + (findAttr "file" "Main" attrs) + (findAttr "namespace" "" attrs) +parseSnippet json = Nothing + +traverseSnippets : Monad m => (Snippet -> m JSON) -> JSON -> m JSON +traverseSnippets f json = traverseJSON (\x => maybe (pure x) f (parseSnippet x)) json + +traverseSnippets_ : Monad m => (Snippet -> m ()) -> JSON -> m () +traverseSnippets_ f json = traverseJSON_ (\x => maybe (pure ()) f (parseSnippet x)) json + +collateCode : JSON -> SnocList Snippet +collateCode doc = execState [<] $ traverseSnippets_ (\snippet => modify (:< snippet)) doc + +covering +writeCode : (dir : String) -> + (snippets : List Snippet) -> + IO (List (Nat, Nat)) +writeCode dir snippets = do + (files, ranges) <- runStateT SortedMap.empty $ traverse (\snippet => do + let fileName = "\{dir}/\{snippet.file}.idr" + + let indentDepth = 0 + + indentDepth <- if snippet.namespace_ /= "" + then do + ignore $ writeBlock fileName indentDepth "namespace \{snippet.namespace_}" + pure $ 1 + indentDepth + else pure indentDepth + + indentDepth <- case snippet.codeType of + Decls => pure indentDepth + Expr exprType => do + let varName = "x\{show $ cast {to = Bits32} !(randomIO {a = Int32})}" + ignore $ writeBlock fileName indentDepth "\{varName} : \{exprType}\n\{varName} =" + pure $ 1 + indentDepth + + writeBlock fileName indentDepth snippet.code + ) snippets + traverse_ (\(file, _) => closeFile file) files + pure ranges + where + indent : Nat -> List String -> List String + indent indentDepth block = do + let indentPrefix = replicate (4 * indentDepth) ' ' + map (\case "" => ""; line => indentPrefix ++ line) block + + getFile : String -> StateT (SortedMap String (File, Nat)) IO (File, Nat) + getFile fileName = do + files <- get + let Nothing = lookup fileName files + | Just file => pure file + + Right file <- openFile fileName WriteTruncate + | Left fileError => die "Error writing Idris code to file: \{show fileError}" + + modify $ insert fileName (file, 1) + pure (file, 1) + + writeBlock : (fileName : String) -> + (indentDepth : Nat) -> + (block : String) -> + StateT (SortedMap String (File, Nat)) IO (Nat, Nat) + writeBlock fileName indentDepth block = do + let ls = indent indentDepth $ lines block + let lineCount = length ls + (file, start) <- getFile fileName + + -- Round trip of `unlines . lines` not identiy + -- This might introduce a new trailing newline + -- Trailing newline important for consistency of line counting + Right () <- fPutStrLn file $ unlines ls + | Left fileError => die "Error writing Idris code to file: \{show fileError}" + + modify $ updateExisting (mapSnd (1 + lineCount +)) fileName + pure (start, minus lineCount 1) + +covering +checkCode : (dir : String) -> + (packages : List String) -> + (snippets : List Snippet) -> + IO () +checkCode dir packages snippets = do + let fileNames = SortedSet.fromList $ map file snippets + for_ fileNames $ \fileName => do + (_, 0) <- run $ ["idris2", "-c", "\{dir}/\{fileName}.idr"] ++ (packages >>= (\package => ["-p", package])) + | (msg, err) => die $ "Error checking Idris code (exit code: \{show err})\n" ++ msg + pure () + +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 + +covering +formatSnippet : (dir : String) -> Snippet -> (start : Nat) -> (len : Nat) -> IO JSON +formatSnippet dir snippet start len = do + let False = snippet.hide + | True => pure $ 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}" + (out, 0) <- run katlaCmd + | (_, err) => die "Error running Katla (exit code: \{show err})" + + let out = if snippet.namespace_ /= "" then dedent out else out + let out = case snippet.codeType of + Decls => out + Expr _ => dedent out + + pure $ JObject [ + ("t", JString $ case snippet.displayType of Block => "RawBlock"; Inline => "RawInline"), + ("c", JArray [ + JString "tex", + JString $ "\\let\\KatlaSnippet\\relax{}" ++ out ++ "\\KatlaSnippet{}" + ]) + ] + where + katlaIndent : String + katlaIndent = "\\KatlaSpace{}\\KatlaSpace{}\\KatlaSpace{}\\KatlaSpace{}" + + katlaIndentLen : Nat + katlaIndentLen = length katlaIndent + + dedent : String -> String + dedent block = unlines $ + map (\line => if isPrefixOf katlaIndent line + then substr katlaIndentLen (minus (length line) katlaIndentLen) line + else line + ) $ + lines block + +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 + +covering +main : IO () +main = do + doc <- getLine + let Just doc = parse doc + | Nothing => pure () + + let snippets = cast $ collateCode doc + let packages = findPackages doc + + let dir = "build/katla" + ignore $ createDir "build" + ignore $ createDir dir + + ranges <- writeCode dir snippets + checkCode dir packages snippets + doc <- addKatlaHeader doc + doc <- addKatlaSnippets dir snippets ranges doc + + printLn doc diff --git a/tests/Main.idr b/tests/Main.idr index bae7e28..66979f8 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -14,6 +14,7 @@ tests = MkTestPool "Examples using Katla" [] Nothing , "init" , "markdown" , "literate" + , "pandoc" ] main : IO () diff --git a/tests/examples/pandoc/Source.md b/tests/examples/pandoc/Source.md new file mode 100644 index 0000000..487879c --- /dev/null +++ b/tests/examples/pandoc/Source.md @@ -0,0 +1,89 @@ +--- +title: Writing an Idris2 PDF file with katla-pandoc +idris2-packages: + - contrib +colorlinks: true # Workaround for conflict between Katla and pandoc default latex template +--- + +Using [katla](https://github.com/idris-community/katla)'s pandoc backend we can produce PDF documents containing semantically highlighted Idris2 code. + +The file you are currently reading is the rendered version of a literate markdown/idris2 file. It is called `Source.md` and contains fenced `idr` blocks. + +# Basic Usage + +We can hide uninteresting code blocks by adding the `hide` attribute. We hide an import of `Data.Vect` here. We won't see anything in the output PDF. + +```{.idr .hide} +import Data.Vect +``` + +We can use all Idris 2 features. Here's an example code block: + +```idr +x : Nat +x = 1 + 2 +``` + +We can use namespaces by adding the `namespace` attribute, such as to provide alternate definitions for functions. Consider this function signature: + +```{.idr namespace="A"} +f : Vect n a -> Vect (n + n) a +``` + +Here's one implementation for `f`{.idr namespace="A" type="Vect 1 Nat -> ?"}: + +```{.idr namespace="A"} +f xs = xs ++ xs +``` + +By repeating the signature in a different namespace, in a hidden code block, I can give an alternate definition: + +```{.idr .hide namespace="B"} +f : Vect n a -> Vect (n + n) a +``` + +```{.idr namespace="B"} +f xs = xs ++ reverse xs +``` + +# Inline Code + +As well as block code, we can have inline code, like `the Nat 3`{.idr}. Here's another: `1 + 2`{.idr}. We can also call the function we previously defined: `f [1, 2, 3]`{.idr namespace="A"}. + +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 `decls` class, we can write an inline declaration: `g : Nat -> Nat`{.idr .decls}. + +By using the `expr` class, we can write a block expression: + +```{.idr .expr type="List Nat"} +[ + 1, + 2, + 3 +] +``` + +# Types + +Sometimes, Idris 2 cannot infer the type of an expression. Is `[1, 2, 3]`{.idr type="List Nat"} a `List Nat`{.idr}, or a `Vect 3 Integer`{.idr}? We can use the `type` attribute to tell Idris 2 which one it should be. + +# Multiple Files + +If you need an import to *not* be available, namespaces are not enough. We can use the `file` attribute to put snippets in separate files. For example, the signature of `f`{.idr namespace="A" type="Vect 1 Nat -> ?"} fails to compile if we use a new file, that hasn't imported `Vect`{.idr}. + +```{.idr file="Another"} +failing "Undefined name Vect." + f : Vect n a -> Vect (n + n) a +``` + +# Packages + +We can add Idris 2 packages to the YAML metadata of the Markdown file, using the `idris2-packages` key. For example, adding `contrib` allows us to use the `Language.JSON` module. + +```{.idr file="Package"} +import Language.JSON + +x : Maybe JSON +x = parse #"{"x": 1, "y": 2}"# +``` diff --git a/tests/examples/pandoc/expected b/tests/examples/pandoc/expected new file mode 100644 index 0000000..e69de29 diff --git a/tests/examples/pandoc/run b/tests/examples/pandoc/run new file mode 100644 index 0000000..f762eba --- /dev/null +++ b/tests/examples/pandoc/run @@ -0,0 +1,8 @@ +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" -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 new file mode 100644 index 0000000..c0021a9 --- /dev/null +++ b/tests/examples/pandoc/source-expected.tex @@ -0,0 +1,160 @@ +Using \href{https://github.com/idris-community/katla}{katla}'s pandoc +backend we can produce PDF documents containing semantically highlighted +Idris2 code. + +The file you are currently reading is the rendered version of a literate +markdown/idris2 file. It is called \texttt{Source.md} and contains +fenced \texttt{idr} blocks. + +\hypertarget{basic-usage}{% +\section{Basic Usage}\label{basic-usage}} + +We can hide uninteresting code blocks by adding the \texttt{hide} +attribute. We hide an import of \texttt{Data.Vect} here. We won't see +anything in the output PDF. + +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{} + +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} +\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{}. + +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. + +\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} +\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}{% +\section{Packages}\label{packages}} + +We can add Idris 2 packages to the YAML metadata of the Markdown file, +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{}