" ++ escapeHtml text ++ "
\n" + htmlBlock (Bullet items) = + "" ++
+ escapeHtml p.bytes ++
+ "\n"
+
||| Convert A2ML document to HTML5
export
toHtml : Doc -> String
-toHtml doc =
+toHtml (MkDoc blocks) =
"\n" ++
"\n" ++
"\n" ++
@@ -75,99 +122,47 @@ toHtml doc =
" \n" ++
"\n" ++
"\n" ++
- docToHtml doc ++
+ htmlBlocks blocks ++
"\n" ++
"\n"
- where
- docToHtml : Doc -> String
- docToHtml (MkDoc blocks) = concatMap blockToHtml blocks
-
- blockToHtml : Block -> String
- blockToHtml (Section s) =
- let level = min 6 (length s.id.raw) -- HTML has h1-h6
- tag = "h" ++ show level
- id_attr = " id=\"" ++ escapeHtml s.id.raw ++ "\""
- in "<" ++ tag ++ id_attr ++ ">" ++
- escapeHtml s.title ++
- "\n" ++
- docToHtml (MkDoc s.body)
-
- blockToHtml (Para text) =
- "" ++ escapeHtml text ++ "
\n" - - blockToHtml (Bullet items) = - "" ++
- escapeHtml p.bytes ++
- "\n"
-- ============================================================================
-- Djot Converter
-- ============================================================================
+mutual
+ djotBlocks : List Block -> String
+ djotBlocks [] = ""
+ djotBlocks (block :: rest) = djotBlock block ++ djotBlocks rest
+
+ djotBlock : Block -> String
+ djotBlock (Section (MkSec sid title body)) =
+ let level = length sid.raw
+ heading = replicate level '#' ++ " " ++ title ++ "\n" ++
+ "{#" ++ sid.raw ++ "}\n\n"
+ in heading ++ djotBlocks body
+ djotBlock (Para text) = text ++ "\n\n"
+ djotBlock (Bullet items) =
+ concatMap (\item => "- " ++ item ++ "\n") items ++ "\n"
+ djotBlock (Figure f) =
+ "!{#" ++ f.id.raw ++ "}[" ++ f.caption ++ "]\n\n"
+ djotBlock (Table t) =
+ "{#" ++ t.id.raw ++ "}\n" ++
+ "**" ++ t.caption ++ "**\n\n"
+ djotBlock (Refs refs) =
+ "## References\n\n" ++
+ concatMap (\r => ": " ++ r.label ++ "\n") refs ++ "\n"
+ djotBlock (Opaque p) =
+ let lang = fromMaybe "" p.lang
+ id_attr = case p.id of
+ Just id => "{#" ++ id.raw ++ "}\n"
+ Nothing => ""
+ in id_attr ++ "``` " ++ lang ++ "\n" ++ p.bytes ++ "\n```\n\n"
+
||| Convert A2ML document to Djot markup
export
toDjot : Doc -> String
-toDjot (MkDoc blocks) = concatMap blockToDjot blocks
- where
- blockToDjot : Block -> String
- blockToDjot (Section s) =
- let level = length s.id.raw
- heading = replicate level '#' ++ " " ++ s.title ++ "\n" ++
- "{#" ++ s.id.raw ++ "}\n\n"
- body = toDjot (MkDoc s.body)
- in heading ++ body
-
- blockToDjot (Para text) = text ++ "\n\n"
-
- blockToDjot (Bullet items) =
- concatMap (\item => "- " ++ item ++ "\n") items ++ "\n"
-
- blockToDjot (Figure f) =
- "!{#" ++ f.id.raw ++ "}[" ++ f.caption ++ "]\n\n"
-
- blockToDjot (Table t) =
- "{#" ++ t.id.raw ++ "}\n" ++
- "**" ++ t.caption ++ "**\n\n"
-
- blockToDjot (Refs refs) =
- "## References\n\n" ++
- concatMap (\r => ": " ++ r.label ++ "\n") refs ++ "\n"
-
- blockToDjot (Opaque p) =
- let lang = fromMaybe "" p.lang
- id_attr = case p.id of
- Just id => "{#" ++ id.raw ++ "}\n"
- Nothing => ""
- in id_attr ++ "``` " ++ lang ++ "\n" ++ p.bytes ++ "\n```\n\n"
+toDjot (MkDoc blocks) = djotBlocks blocks
-- ============================================================================
-- LaTeX Converter
@@ -190,10 +185,57 @@ escapeTex str = pack (concatMap escape (unpack str))
escape '~' = unpack "\\~{}"
escape c = [c]
+mutual
+ latexBlocks : List Block -> String
+ latexBlocks [] = ""
+ latexBlocks (block :: rest) = latexBlock block ++ latexBlocks rest
+
+ latexBlock : Block -> String
+ latexBlock (Section (MkSec sid title body)) =
+ let level = length sid.raw
+ command = case level of
+ 1 => "\\section"
+ 2 => "\\subsection"
+ 3 => "\\subsubsection"
+ 4 => "\\paragraph"
+ _ => "\\subparagraph"
+ label = "\\label{" ++ sid.raw ++ "}"
+ in command ++ "{" ++ escapeTex title ++ "}" ++ label ++ "\n" ++
+ latexBlocks body ++ "\n"
+ latexBlock (Para text) = escapeTex text ++ "\n\n"
+ latexBlock (Bullet items) =
+ "\\begin{itemize}\n" ++
+ concatMap (\item => " \\item " ++ escapeTex item ++ "\n") items ++
+ "\\end{itemize}\n\n"
+ latexBlock (Figure f) =
+ "\\begin{figure}[h]\n" ++
+ " \\centering\n" ++
+ " % Insert figure here\n" ++
+ " \\caption{" ++ escapeTex f.caption ++ "}\n" ++
+ " \\label{fig:" ++ f.id.raw ++ "}\n" ++
+ "\\end{figure}\n\n"
+ latexBlock (Table t) =
+ "\\begin{table}[h]\n" ++
+ " \\centering\n" ++
+ " \\caption{" ++ escapeTex t.caption ++ "}\n" ++
+ " \\label{tab:" ++ t.id.raw ++ "}\n" ++
+ " % Insert table here\n" ++
+ "\\end{table}\n\n"
+ latexBlock (Refs refs) =
+ "\\section*{References}\n" ++
+ "\\begin{enumerate}\n" ++
+ concatMap (\r => " \\item " ++ escapeTex r.label ++ "\n") refs ++
+ "\\end{enumerate}\n\n"
+ latexBlock (Opaque p) =
+ let lang = fromMaybe "" p.lang
+ in "\\begin{lstlisting}[language=" ++ lang ++ "]\n" ++
+ p.bytes ++ "\n" ++
+ "\\end{lstlisting}\n\n"
+
||| Convert A2ML document to LaTeX
export
toLatex : Doc -> String
-toLatex doc =
+toLatex (MkDoc blocks) =
"\\documentclass{article}\n" ++
"\\usepackage[utf8]{inputenc}\n" ++
"\\usepackage{hyperref}\n" ++
@@ -201,98 +243,47 @@ toLatex doc =
"\n" ++
"\\begin{document}\n" ++
"\n" ++
- docToTex doc ++
+ latexBlocks blocks ++
"\n" ++
"\\end{document}\n"
- where
- docToTex : Doc -> String
- docToTex (MkDoc blocks) = concatMap blockToTex blocks
-
- blockToTex : Block -> String
- blockToTex (Section s) =
- let level = length s.id.raw
- command = case level of
- 1 => "\\section"
- 2 => "\\subsection"
- 3 => "\\subsubsection"
- 4 => "\\paragraph"
- _ => "\\subparagraph"
- label = "\\label{" ++ s.id.raw ++ "}"
- in command ++ "{" ++ escapeTex s.title ++ "}" ++ label ++ "\n" ++
- docToTex (MkDoc s.body) ++ "\n"
-
- blockToTex (Para text) =
- escapeTex text ++ "\n\n"
-
- blockToTex (Bullet items) =
- "\\begin{itemize}\n" ++
- concatMap (\item => " \\item " ++ escapeTex item ++ "\n") items ++
- "\\end{itemize}\n\n"
-
- blockToTex (Figure f) =
- "\\begin{figure}[h]\n" ++
- " \\centering\n" ++
- " % Insert figure here\n" ++
- " \\caption{" ++ escapeTex f.caption ++ "}\n" ++
- " \\label{fig:" ++ f.id.raw ++ "}\n" ++
- "\\end{figure}\n\n"
-
- blockToTex (Table t) =
- "\\begin{table}[h]\n" ++
- " \\centering\n" ++
- " \\caption{" ++ escapeTex t.caption ++ "}\n" ++
- " \\label{tab:" ++ t.id.raw ++ "}\n" ++
- " % Insert table here\n" ++
- "\\end{table}\n\n"
-
- blockToTex (Refs refs) =
- "\\section*{References}\n" ++
- "\\begin{enumerate}\n" ++
- concatMap (\r => " \\item " ++ escapeTex r.label ++ "\n") refs ++
- "\\end{enumerate}\n\n"
-
- blockToTex (Opaque p) =
- let lang = fromMaybe "" p.lang
- in "\\begin{lstlisting}[language=" ++ lang ++ "]\n" ++
- p.bytes ++ "\n" ++
- "\\end{lstlisting}\n\n"
-- ============================================================================
-- Plain Text Converter
-- ============================================================================
+numberedRefs : Nat -> List Ref -> String
+numberedRefs _ [] = ""
+numberedRefs n (ref :: rest) =
+ show n ++ ". " ++ ref.label ++ "\n" ++ numberedRefs (S n) rest
+
+mutual
+ plainTextBlocks : List Block -> String
+ plainTextBlocks [] = ""
+ plainTextBlocks (block :: rest) =
+ plainTextBlock block ++ plainTextBlocks rest
+
+ plainTextBlock : Block -> String
+ plainTextBlock (Section (MkSec _ title body)) =
+ title ++ "\n" ++
+ replicate (length title) '=' ++ "\n\n" ++
+ plainTextBlocks body
+ plainTextBlock (Para text) = text ++ "\n\n"
+ plainTextBlock (Bullet items) =
+ concatMap (\item => "* " ++ item ++ "\n") items ++ "\n"
+ plainTextBlock (Figure f) =
+ "[Figure: " ++ f.caption ++ "]\n\n"
+ plainTextBlock (Table t) =
+ "[Table: " ++ t.caption ++ "]\n\n"
+ plainTextBlock (Refs refs) =
+ "References\n" ++
+ "==========\n\n" ++
+ numberedRefs 1 refs ++ "\n"
+ plainTextBlock (Opaque p) = p.bytes ++ "\n\n"
+
||| Convert A2ML document to plain text (no formatting)
export
toPlainText : Doc -> String
-toPlainText (MkDoc blocks) = concatMap blockToText blocks
- where
- blockToText : Block -> String
- blockToText (Section s) =
- s.title ++ "\n" ++
- replicate (length s.title) '=' ++ "\n\n" ++
- toPlainText (MkDoc s.body)
-
- blockToText (Para text) = text ++ "\n\n"
-
- blockToText (Bullet items) =
- concatMap (\item => "* " ++ item ++ "\n") items ++ "\n"
-
- blockToText (Figure f) =
- "[Figure: " ++ f.caption ++ "]\n\n"
-
- blockToText (Table t) =
- "[Table: " ++ t.caption ++ "]\n\n"
-
- blockToText (Refs refs) =
- "References\n" ++
- "==========\n\n" ++
- concatMap (\r => show (1 + elemIndex r refs) ++ ". " ++ r.label ++ "\n") refs ++ "\n"
- where
- elemIndex : Eq a => a -> List a -> Nat
- elemIndex x [] = 0
- elemIndex x (y :: ys) = if x == y then 0 else 1 + elemIndex x ys
-
- blockToText (Opaque p) = p.bytes ++ "\n\n"
+toPlainText (MkDoc blocks) = plainTextBlocks blocks
-- ============================================================================
-- Converter Selection
@@ -344,6 +335,23 @@ testMarkdownRoundTrip doc =
Success doc' _ => length (blocks doc) == length (blocks doc')
_ => False
+mutual
+ extractContent : Doc -> String
+ extractContent (MkDoc blocks) = extractBlocks blocks
+
+ extractBlocks : List Block -> String
+ extractBlocks [] = ""
+ extractBlocks (block :: rest) = extractBlock block ++ extractBlocks rest
+
+ extractBlock : Block -> String
+ extractBlock (Section (MkSec _ title body)) = title ++ extractBlocks body
+ extractBlock (Para text) = text
+ extractBlock (Bullet items) = concatMap id items
+ extractBlock (Figure f) = f.caption
+ extractBlock (Table t) = t.caption
+ extractBlock (Refs refs) = concatMap (\r => r.label) refs
+ extractBlock (Opaque p) = p.bytes
+
||| Test if A2ML → Plain Text → A2ML preserves content
export
partial
@@ -353,15 +361,3 @@ testPlainTextRoundTrip doc =
content1 = extractContent doc
content2 = txt
in length content1 == length content2
- where
- extractContent : Doc -> String
- extractContent (MkDoc blocks) = concatMap extractBlock blocks
-
- extractBlock : Block -> String
- extractBlock (Section s) = s.title ++ extractContent (MkDoc s.body)
- extractBlock (Para text) = text
- extractBlock (Bullet items) = concatMap id items
- extractBlock (Figure f) = f.caption
- extractBlock (Table t) = t.caption
- extractBlock (Refs refs) = concatMap (\r => r.label) refs
- extractBlock (Opaque p) = p.bytes