From b0f0d93440d71179a5ac2185dc756a56a38abafe Mon Sep 17 00:00:00 2001
From: "Achim D. Brucker" <adbrucker@0x5f.org>
Date: Mon, 21 Jan 2019 16:57:04 +0000
Subject: [PATCH] Initial document generation support.

---
 .gitignore                |  1 +
 Hiding_Type_Variables.thy |  2 +-
 ROOT                      |  4 +-
 document/root.tex         | 89 +++++++++++++++++++++++++++++++++++++++
 4 files changed, 94 insertions(+), 2 deletions(-)
 create mode 100644 document/root.tex

diff --git a/.gitignore b/.gitignore
index eaf16c5..cc06046 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,2 +1,3 @@
 example01.json
 *~
+output
diff --git a/Hiding_Type_Variables.thy b/Hiding_Type_Variables.thy
index eb3bc2c..f79fcbd 100644
--- a/Hiding_Type_Variables.thy
+++ b/Hiding_Type_Variables.thy
@@ -57,7 +57,7 @@ text\<open>
   of overriding a suffice (or prefix) of the default type variables. For 
   example, \<open>('state) hide_tvar_foo _.\<close> is a short-hand for 
   \<open>('a, 'b, 'c, 'd, 'state) hide_tvar_foo\<close>.
-}\<close>
+\<close>
 
 section\<open>Implementation\<close>
 subsection\<open>Theory Managed Data Structure\<close>
diff --git a/ROOT b/ROOT
index 842c958..84372db 100644
--- a/ROOT
+++ b/ROOT
@@ -1,6 +1,8 @@
 session "isabelle-hacks" = "HOL" +
-  options [document = false]
+  options [timeout = 600, document = pdf, document_variants="document:outline=/proof,/ML",document_output=output]
   theories
     Assert
     Hiding_Type_Variables
     Nano_JSON
+  document_files
+    root.tex
diff --git a/document/root.tex b/document/root.tex
new file mode 100644
index 0000000..1db6b45
--- /dev/null
+++ b/document/root.tex
@@ -0,0 +1,89 @@
+\documentclass[10pt,DIV16,a4paper,abstract=true,twoside=semi,openright]
+{scrreprt}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%% Overrides the (rightfully issued) warnings by Koma Script that \rm
+%%% etc. should not be used (they are deprecated since more than a
+%%% decade)
+  \DeclareOldFontCommand{\rm}{\normalfont\rmfamily}{\mathrm}
+  \DeclareOldFontCommand{\sf}{\normalfont\sffamily}{\mathsf}
+  \DeclareOldFontCommand{\tt}{\normalfont\ttfamily}{\mathtt}
+  \DeclareOldFontCommand{\bf}{\normalfont\bfseries}{\mathbf}
+  \DeclareOldFontCommand{\it}{\normalfont\itshape}{\mathit}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\usepackage[USenglish]{babel}
+\usepackage[numbers, sort&compress]{natbib}
+\usepackage{isabelle,isabellesym}
+\usepackage{booktabs}
+\usepackage{paralist}
+\usepackage{graphicx}
+\usepackage{amssymb}
+\usepackage{xspace}
+\usepackage{xcolor}
+\usepackage{listings}
+\lstloadlanguages{HTML}
+\usepackage[]{mathtools}
+\usepackage[pdfpagelabels, pageanchor=false, plainpages=false]{hyperref}
+\lstdefinestyle{html}{language=XML,
+  basicstyle=\ttfamily,
+  commentstyle=\itshape,
+  keywordstyle=\color{blue},
+  ndkeywordstyle=\color{blue},
+}
+\lstdefinestyle{displayhtml}{style=html,
+  floatplacement={tbp},
+  captionpos=b,
+  framexleftmargin=0pt,
+  basicstyle=\ttfamily\scriptsize,
+  backgroundcolor=\color{black!2},
+  frame=lines,
+}
+\lstnewenvironment{html}[1][]{\lstset{style=displayhtml, #1}}{}
+\def\inlinehtml{\lstinline[style=html, columns=fullflexible]}
+
+\pagestyle{headings}
+\isabellestyle{default}
+\setcounter{tocdepth}{1}
+\newcommand{\ie}{i.\,e.\xspace}
+\newcommand{\eg}{e.\,g.\xspace}
+\newcommand{\thy}{\isabellecontext}
+\renewcommand{\isamarkupsection}[1]{%
+  \begingroup% 
+  \def\isacharunderscore{\textunderscore}%
+  \section{#1 (\thy)}%
+  \def\isacharunderscore{-}%
+  \expandafter\label{sec:\isabellecontext}%
+  \endgroup% 
+}
+\newcommand{\isactrltype}{\\<\^type>}
+\title{Isabelle Hacks}
+\author{Achim~D.~Brucker}%
+\publishers{}
+\begin{document}
+  \maketitle
+  \begin{abstract}
+    \begin{quote}
+      This project contains small Isabelle ``hacks'' that provide additional
+      functionality to \href{https://isabelle.in.tum.de}{Isabelle} or showcase
+      specific functionality. The individual hacks usually consist out of 
+      a single theory file and all documentation is contained in that 
+      theory file. The master branch should work with the latest official 
+      release of Isabelle (Isabelle 2018, at time of writing), hacks for 
+      older versions might be available on a dedicated branch.
+
+    %\bigskip
+    %\noindent{\textbf{Keywords:}} 
+    \end{quote}
+  \end{abstract}
+
+
+\tableofcontents
+\cleardoublepage
+
+\input{session}
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End: