From 8bd1d46961b41cc643810fc028c4127279463c36 Mon Sep 17 00:00:00 2001
From: Alex Richardson
Date: Mon, 28 Sep 2020 12:01:04 +0100
Subject: Handle sectioning commands in saildoc LaTeX output

---
 src/latex.ml                         |  4 ++++
 test/latex/candperm.commands.tex.exp | 14 ++++++++++++++
 test/latex/candperm.sail             | 18 ++++++++++++++++++
 3 files changed, 36 insertions(+)

diff --git a/src/latex.ml b/src/latex.ml
index 6d479a52..3804d07b 100644
--- a/src/latex.ml
+++ b/src/latex.ml
@@ -266,6 +266,10 @@ let latex_of_markdown str =
        "\\begin{enumerate}\n\\item "
        ^ Util.string_of_list "\n\\item " format list
        ^ "\n\\end{enumerate}"
+    | H1 header -> "\\section*{" ^ (format header) ^ "}\n"
+    | H2 header -> "\\subsection*{" ^ (format header) ^ "}\n"
+    | H3 header -> "\\subsubsection*{" ^ (format header) ^ "}\n"
+    | H4 header -> "\\paragraph*{" ^ (format header) ^ "}\n"
     | Br -> "\n"
     | NL -> "\n"
     | elem -> failwith ("Can't convert to latex: " ^ Omd_backend.sexpr_of_md [elem])
diff --git a/test/latex/candperm.commands.tex.exp b/test/latex/candperm.commands.tex.exp
index df253d71..561975f5 100644
--- a/test/latex/candperm.commands.tex.exp
+++ b/test/latex/candperm.commands.tex.exp
@@ -39,6 +39,20 @@ and bits \firstUPerm{} .. \lastUPerm{} of \emph{rd}.
 
 }{\lstinputlisting[language=sail]{out/fclCAndPermMarkdownWithRefMacrozexecute33a689e3a631b9b905b85461d3814943.tex}}}}
 
+\newcommand{\sailfclCAndPermMarkdownWithExceptionsexecute}{\saildoclabelled{fclCAndPermMarkdownWithExceptionszexecute}{\saildocfcl{Capability register \emph{cd} is replaced with the contents of capability
+register \emph{cs1} with the \cperms{} field set to the bitwise-AND of
+its previous value and bits 0 .. 10 of integer register \emph{rs2}
+and the \cuperms{} field set to the bitwise and of its previous value
+and bits \firstUPerm{} .. \lastUPerm{} of \emph{rd}.
+
+\subsubsection*{Exceptions:}
+An exception is raised if:
+
+\begin{itemize}
+\item \emph{cs1.tag} is not set.
+\item \emph{cs1} is sealed.
+\end{itemize}}{\lstinputlisting[language=sail]{out/fclCAndPermMarkdownWithExceptionszexecute33a689e3a631b9b905b85461d3814943.tex}}}}
+
 
 
 \newcommand{\sailval}[1]{
diff --git a/test/latex/candperm.sail b/test/latex/candperm.sail
index 75482db1..656818d2 100644
--- a/test/latex/candperm.sail
+++ b/test/latex/candperm.sail
@@ -63,5 +63,23 @@ function clause execute(CAndPermMarkdownWithRefMacro(cd, cs1, rs2)) = {
     return ()
 }
 
+union clause ast = CAndPermMarkdownWithExceptions : (int, int, int)
+/*!
+ * Capability register *cd* is replaced with the contents of capability
+ * register *cs1* with the \cperms{} field set to the bitwise-AND of
+ * its previous value and bits 0 .. 10 of integer register *rs2*
+ * and the \cuperms{} field set to the bitwise and of its previous value
+ * and bits \firstUPerm{} .. \lastUPerm{} of *rd*.
+ *
+ * ### Exceptions:
+ * An exception is raised if:
+ *   - *cs1.tag* is not set.
+ *   - *cs1* is sealed.
+ */
+function clause execute(CAndPermMarkdownWithExceptions(cd, cs1, rs2)) = {
+    /* Implementation */
+    return ()
+}
+
 end execute
 end ast
-- 
cgit v1.2.3


From 263ffca94d22e1ff7ce32d8f6ba782b0fcacd0d7 Mon Sep 17 00:00:00 2001
From: Alex Richardson
Date: Mon, 28 Sep 2020 12:03:26 +0100
Subject: LaTeX: Add newline after itemize and enumerate environments

---
 src/latex.ml                         | 4 ++--
 test/latex/candperm.commands.tex.exp | 3 ++-
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/src/latex.ml b/src/latex.ml
index 3804d07b..381fc649 100644
--- a/src/latex.ml
+++ b/src/latex.ml
@@ -261,11 +261,11 @@ let latex_of_markdown str =
     | (Ul list | Ulp list) ->
        "\\begin{itemize}\n\\item "
        ^ Util.string_of_list "\n\\item " format list
-       ^ "\n\\end{itemize}"
+       ^ "\n\\end{itemize}\n"
     | (Ol list | Olp list) ->
        "\\begin{enumerate}\n\\item "
        ^ Util.string_of_list "\n\\item " format list
-       ^ "\n\\end{enumerate}"
+       ^ "\n\\end{enumerate}\n"
     | H1 header -> "\\section*{" ^ (format header) ^ "}\n"
     | H2 header -> "\\subsection*{" ^ (format header) ^ "}\n"
     | H3 header -> "\\subsubsection*{" ^ (format header) ^ "}\n"
diff --git a/test/latex/candperm.commands.tex.exp b/test/latex/candperm.commands.tex.exp
index 561975f5..14153396 100644
--- a/test/latex/candperm.commands.tex.exp
+++ b/test/latex/candperm.commands.tex.exp
@@ -51,7 +51,8 @@ An exception is raised if:
 \begin{itemize}
 \item \emph{cs1.tag} is not set.
 \item \emph{cs1} is sealed.
-\end{itemize}}{\lstinputlisting[language=sail]{out/fclCAndPermMarkdownWithExceptionszexecute33a689e3a631b9b905b85461d3814943.tex}}}}
+\end{itemize}
+}{\lstinputlisting[language=sail]{out/fclCAndPermMarkdownWithExceptionszexecute33a689e3a631b9b905b85461d3814943.tex}}}}
 
 
 
-- 
cgit v1.2.3