Handle sectioning commands in saildoc LaTeX output

rems-project · Sep 28, 2020 · 8bd1d46 · 8bd1d46
1 parent 882850d
commit 8bd1d46
Show file tree

Hide file tree

Showing 3 changed files with 36 additions and 0 deletions.
diff --git 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
@@ -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
@@ -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