Various layout improvements.

examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy

@@ -78,6 +78,36 @@ generation and ways to adapt it to particular purposes.
  Finally, we draw 
 conclusions  and discuss related work in @{docitem_ref (unchecked) \<open>conclusion\<close>}. \<close>  
 
+
+section\<open>Notation and Layout Conventions\<close>
+text\<open>
+  We acknowledge that understanding \isadof and its implementation in all details requires
+  to separate multiple technological layers or languages. To help the reader with this, we 
+  will type-set the different languages in different styles. In particular, we will use 
+  \<^item> a light-blue background for input written in Isabelle's Isar language, \eg:
+    \begin{isar}
+    lemma refl: "x = x" 
+      by simp
+    \end{isar}
+  \<^item> For small examples of generated document, we use a green background:
+    \begin{out}
+    The axiom refl
+    \end{out}
+  \<^item> For (S)ML-code, we use a red background:
+    \begin{sml}
+    fun id x = x
+    \end{sml}
+  \<^item> \LaTeX-code, we use a yellow background:
+    \begin{ltx}
+    \newcommand{\refl}{$x = x$}
+    \end{ltx}
+  \<^item> For shell scripts and interative shell sessions, we use a grey background:
+    \begin{bash}
+    > ls 
+   \end{bash}
+
+\<close>
+
 (*<*) 
 end
 (*>*) 

examples/technical_report/Isabelle_DOF-Manual/02_Background.thy

@@ -57,34 +57,6 @@ document model, and than explain how Isabelle as a framework fits into this pict
 \<close>
 
 
-(*
-Thus, a user can add a simple text:
-\begin{isar}
-  text\<Open>This is a description.\<Close>
-\end{isar}
-These text-commands can be arbitrarily mixed with other commands stating definitions, proofs, code, etc.,
-and will result in the corresponding output in generated \LaTeX{} or HTML documents. 
-Now, \<^emph>\<open>inside\<close> the textual content, it is possible to embed a \<^emph>\<open>text-antiquotation\<close>:
-\begin{isar}
-  text\<Open>According to the reflexivity axiom \at{thm refl}, we obtain in \<Gamma> 
-           for \at{term "fac 5"} the result \at{value "fac 5"}.\<Close>
-\end{isar}
-which is represented in the generated output by:
-\begin{out}
-  According to the reflexivity axiom $x = x$, we obtain in $\Gamma$ for $\operatorname{fac} 5$ the result $120$.
-\end{out}
-where \inlineisar+refl+ is actually the reference to the axiom of reflexivity in HOL. 
-For the antiquotation \inlineisar+\at{value "fac 5"}+  we assume the usual definition for 
-\inlineisar+fac+ in HOL.
-\<close>
-
-text*[anti]\<open> Thus, antiquotations can refer to formal content, can be type-checked before being 
-displayed and can be used for calculations before actually being typeset. When editing, 
-Isabelle's PIDE offers auto-completion and error-messages while typing the above 
-\<^emph>\<open>semi-formal\<close> content.  \<close>
-*)
-
-
 section*["sec:background"::introduction]\<open>The Required Document Model\<close>
 text\<open>
 In this section, we explain the assumed document model underlying
@@ -146,12 +118,12 @@ However, this translation is not necessarily one-to-one: text
 elements can be enriched by formal, \ie, machine-checked content via
 \emph{semantic macros}, called antiquotations:
 \begin{isar}
-  text\<Open>According to the reflexivity axiom @{thm refl}, we obtain in \<Gamma> 
-        for @{term "fac 5"} the result @{value "fac 5"}.\<Close>
+  text\<Open>According to the reflexivity axiom <@>{thm refl}, we obtain in \<Gamma> 
+        for <@>{term "fac 5"} the result <@>{value "fac 5"}.\<Close>
 \end{isar}
 which is represented in the final document (\eg, a PDF) by:
 \begin{out}
-  According to the reflexivity axiom $x = x$, we obtain in $\Gamma$ for $\operatorname{fac} 5$ the result $120$.
+  According to the reflexivity axiom $\mathrm{x = x}$, we obtain in $\Gamma$ for $\operatorname{fac} \text{\textrm{5}}$ the result $\text{\textrm{120}}$.
 \end{out}
 Semantic macros are partial functions of type %
 \inlineisar+\<theta> \<rightarrow> text+; since they can use the

examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy

@@ -514,10 +514,10 @@ Where \inlineisar+title*[a ...]+ is a predefined macro for
 \inlineisar+text*[a::title,...]\<Open>...\<Close>+ (similarly \inlineisar+abstract*+). 
 The macro \inlineisar+section*+ assumes a class-id referring to a class that has 
 a \inlineisar+level+ attribute. We continue our example text:
-\begin{isar}
+\begin{isar}[mathescape]
 text*[c1::contrib_claim, based_on="[''pumps'',''steam boiler'']" ]\<Open>
-  As indicated in @{introduction "intro"}, we the water level of the
-  boiler is always between the minimum and the maximum allowed level.
+  As indicated in <@>{introduction "intro"}, we the water level of the
+  boiler is always between the minimum a$$nd the maximum allowed level.
 \<Close>
 \end{isar}
 \<close>
@@ -526,7 +526,7 @@ The first text element in this example fragment \<^emph>\<open>defines\<close> t
 text entity \inlineisar+c1+ and also references the formerly defined
 text element \inlineisar+intro+ (which will be represented in the PDF
 output, for example, by a text anchor ``Section 1'' and a hyperlink to
-its beginning). The antiquotation \inlineisar+<At>{introduction ...}+,
+its beginning). The antiquotation \inlineisar+<@>{introduction ...}+,
 which is automatically generated from the ontology, is immediately
 validated (the link to \inlineisar+intro+ is defined) and type-checked (it
 is indeed a link to an \inlineisar+introduction+
@@ -599,6 +599,7 @@ text\<open>The syntax of toplevel \isadof commands reads as follows:
        | @@{command "Definition*"} | @@{command "Lemma*"} 
        | @@{command "Theorem*"}  | @@{command "Conjecture*"} 
        ) 
+       \<newline>
        '[' meta_args ']' '\<open>' text '\<close>'
      ) 
      | change_status_command

examples/technical_report/Isabelle_DOF-Manual/06_Conclusion.thy

@@ -52,18 +52,6 @@ text\<open> \isadof in its present form has a number of technical short-comings
   order.\<close>
 
 
-
-subsubsection\<open>Availability.\<close>
-text\<open> The implementation of the framework is available at
- @{url \<open>https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF/\<close>}.
-\isadof is licensed under a 2-clause BSD license (SPDX-License-Identifier: BSD-2-Clause).\<close>
-
-
-subsubsection\<open>Acknowledgments.\<close>
-text\<open>This work has been partially supported by IRT SystemX, Paris-Saclay, France, and 
-therefore granted with public funds of the Program ``Investissements d'Avenir.''\<close> 
-
-
 (*<*) 
 end
 (*>*) 

examples/technical_report/Isabelle_DOF-Manual/document/lstisadof.sty

@@ -59,8 +59,8 @@
     \def\endlstdelim{\texttt{\textbf{\color{black!60}#2}}\egroup}%
     \ttfamily\textbf{\color{black!60}#1}\bgroup\rmfamily\color{#3}\aftergroup\endlstdelim%
 }
-\newcommand{\subscr}[1]{\ensuremath{_{\mbox{#1}}}}
-\newcommand{\supscr}[1]{\ensuremath{^{\mbox{#1}}}}
+\newcommand{\subscr}[1]{\ensuremath{_{\text{#1}}}}
+\newcommand{\supscr}[1]{\ensuremath{^{\text{#1}}}}
 \lstdefinestyle{ISAR}{%
   language=%
   ,basicstyle=\ttfamily%
@@ -72,10 +72,18 @@
   % ,moredelim=*[s][\rmfamily]{\{*}{*\}}%
   ,moredelim = **[is][\beginlstdelim{\{*}{*\}}{black}]{\{*}{*\}}
   ,showstringspaces=false%
-  ,moredelim=*[is][\supscr]{\\<^bsup>}{\\<^esup>}%
+  ,moredelim=*[is][\supscr]{<bsup>}{<esup>}%
+  ,moredelim=*[is][\subscr]{<bsub>}{<esub>}%
   ,literate={%
     {...}{\,\ldots\,}3%
-    {[*]}{\textbullet}1%
+    {<Open>}{\ensuremath{\isacartoucheopen}}1%
+    {<open>}{\ensuremath{\isacartoucheopen}}1%
+    {<@>}{@}1%
+    {"}{}0%
+    {~}{\ }1%
+    {::}{:\!:}1%
+    {<Close>}{\ensuremath{\isacartoucheclose}}1%
+    {<close>}{\ensuremath{\isacartoucheclose}}1%
     {\\<Gamma>}{\ensuremath{\Gamma}}1%
     {\\<theta>}{\ensuremath{\theta}}1%
     {\\<times>}{\ensuremath{\times}}1%
@@ -85,13 +93,32 @@
     {level0}{level\textsubscript{0}}6%
     {\\<Rightarrow>}{\ensuremath{\Rightarrow}}1%
     {\\<rightarrow>}{\ensuremath{\rightarrow}}1%
+    {\\<longrightarrow>}{\ensuremath{\rightarrow}}1%
+    {\\<and>}{\ensuremath{\land}}1%  
+    {\\<or>}{\ensuremath{\lor}}1%
+    {\\<lfloor>}{\ensuremath{\lfloor}}1%
+    {\\<rfloor>}{\ensuremath{\rfloor}}1%  
+    %{\\<lparr>}{\ensuremath{\lparr}}1% 
+    %{\\<rparr>}{\ensuremath{\rparr}}1%
+    {\\<le>}{\ensuremath{\le}}1%
+    {\\<delta>}{\ensuremath{\delta}}1%
+    {\\<lambda>}{\ensuremath{\lambda}}1%
+    {\\<bar>}{\ensuremath{\vert}}1%
+    {\<sigma>}{\ensuremath{\sigma}}1%
+    {\\<lparr>}{\ensuremath{\isasymlparr}}1%  
+    {\\<rparr>}{\ensuremath{\isasymrparr}}1% 
     {\\<leftrightarrow>}{\ensuremath{\leftrightarrow}}1%
     {\{*}{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}1%
     {*\}}{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}1%
     {\\<open>}{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}1%
+    {\\<Open>}{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}1%
     {\\<close>}{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}1%
+    {\\<Close>}{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}1%
     {\\<forall>}{\ensuremath{\forall}}1%
+    {\\<exists>}{\ensuremath{\exists}}1%
     {\\<in>}{\ensuremath{\in}}1%
+    {\\<delta>}{\ensuremath{\delta}}1%
+    {\\<real>}{\ensuremath{\mathbb{R}}}1%
     {¥}{}0%
     {\\<noteq>}{\ensuremath{\neq}}1%
     {\\<exists>}{\ensuremath{\exists}}1%
@@ -111,18 +138,18 @@
    % Defining 2-keywords
    ,keywordstyle=[2]{\color{Blue!60}\bfseries}%
    ,alsoletter={*,-}
-   ,morekeywords=[2]{theory, begin, end, ML,section,subsection,paragraph,chapter,text,setup}%
+   ,morekeywords=[2]{case, then, show, theory, begin, end, ML,section,subsection,paragraph,chapter,text}%
    %,moredelim=[s][\textit]{<}{>}
    % Defining 3-keywords
    ,keywordstyle=[3]{\color{OliveGreen!60}\bfseries}%
    ,morekeywords=[3]{doc_class,declare_reference,update_instance*,
-     open_monitor*, close_monitor*, declare_reference*,section*,subsection*,text*,title*,abstract*}%
+     open_monitor*,  close_monitor*, declare_reference*,section*,text*,title*,abstract*}%
    % Defining 4-keywords
    ,keywordstyle=[4]{\color{black!60}\bfseries}%
    ,morekeywords=[4]{where, imports, keywords}%
    % Defining 5-keywords
    ,keywordstyle=[5]{\color{BrickRed!70}\bfseries}%
-   ,morekeywords=[5]{datatype, definition, type_synonym, typedecl, consts, theorem}%
+   ,morekeywords=[5]{datatype, by, fun, Definition*, definition, type_synonym, typedecl, consts, assumes, and, shows, proof, next, qed, lemma, theorem}%
    % Defining 6-keywords
    ,keywordstyle=[6]{\itshape}%
    ,morekeywords=[6]{meta-args, ref, expr, class_id}%
@@ -130,14 +157,14 @@
 }%
 %% 
 \lstnewenvironment{isar}[1][]{\lstset{style=ISAR,
-    backgroundcolor=\color{black!4},
-    frame=lines,
+    backgroundcolor=\color{blue!6},
+    frame=lines,mathescape,
     basicstyle=\footnotesize\ttfamily,#1}}{}
 %%% 
 \def\inlineisar{\lstinline[style=ISAR,breaklines=true,mathescape,breakatwhitespace=true]}
 
 \lstnewenvironment{out}[1][]{\lstset{
-    backgroundcolor=\color{green!4},
+    backgroundcolor=\color{green!6},
     frame=lines,mathescape,breakatwhitespace=true
     ,columns=flexible%
     ,basicstyle=\footnotesize\rmfamily,#1}}{}
@@ -146,62 +173,17 @@
 %%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%
 \lstloadlanguages{ML}
-\lstdefinestyle{sml}{%
-  basicstyle=\ttfamily%
-  ,showspaces=false%
-  ,showlines=false%
-  ,columns=flexible%
-  ,keepspaces
-  ,morecomment=[s]{(*}{*)}%
-   ,commentstyle=\itshape%
-  % ,moredelim=*[s][\rmfamily]{\{*}{*\}}%
-  ,moredelim = **[is][\beginlstdelim{\{*}{*\}}{black}]{\{*}{*\}}
-  ,showstringspaces=false%
-  ,moredelim=*[is][\supscr]{\\<^bsup>}{\\<^esup>}%
-   ,language=ML%
-  ,literate={%
-    {...}{\,\ldots\,}3%
-    {[*]}{\textbullet}1%
-    {\\<Gamma>}{\ensuremath{\Gamma}}1%
-    {\\<theta>}{\ensuremath{\theta}}1%
-    {\\<times>}{\ensuremath{\times}}1%
-    {\\<equiv>}{\ensuremath{\equiv}}1%
-    {\\<sigma>}{\ensuremath{\sigma}}1%
-    {\\<geq>}{\ensuremath{\geq}}1%
-    {level0}{level\textsubscript{0}}6%
-    {\\<Rightarrow>}{\ensuremath{\Rightarrow}}1%
-    {\\<rightarrow>}{\ensuremath{\rightarrow}}1%
-    {\\<leftrightarrow>}{\ensuremath{\leftrightarrow}}1%
-    {\{*}{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}1%
-    {*\}}{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}1%
-    {\\<open>}{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}1%
-    {\\<close>}{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}1%
-    {\\<forall>}{\ensuremath{\forall}}1%
-    {\\<in>}{\ensuremath{\in}}1%
-    {¥}{}0%
-    {\\<noteq>}{\ensuremath{\neq}}1%
-    {\\<exists>}{\ensuremath{\exists}}1%
-    {\\<Forall>}{\ensuremath{\bigwedge\,}}1%
-    {\\<lbrakk>}{\ensuremath{\mathopen{\lbrack\mkern-3mu\lbrack}}}1%
-    {\\<lbrace>}{\ensuremath{\mathopen{\lbrace\mkern-4.5mu\mid}}}1%
-    {\\<rbrakk>}{\ensuremath{\mathclose{\rbrack\mkern-3mu\rbrack}}}1%
-    {\\<rbrace>}{\ensuremath{\mathclose{\mid\mkern-4.5mu\rbrace}}}1%
-  }%
-  % % Defining "tags" (text-antiquotations) based on 1-keywords
-   ,tag=**[s]{@\{}{\}}%
-   ,tagstyle=\color{CornflowerBlue}%
-   ,markfirstintag=true%
-   ,keywordstyle=\bfseries%
-   %,keywords={}
-  % 
-   ,keywordstyle=\bfseries\color{CornflowerBlue}%
-   ,ndkeywordstyle=\color{red}%
+\lstdefinestyle{sml}{basicstyle=\ttfamily,%
+                     commentstyle=\itshape,%
+                     keywordstyle=\bfseries\color{CornflowerBlue},%
+                     ndkeywordstyle=\color{red},%
+                     language=ML,
    ,keywordstyle=[6]{\itshape}%
    ,morekeywords=[6]{args_type}%
 }%
 
 \lstnewenvironment{sml}[1][]{\lstset{style=sml,
-    backgroundcolor=\color{red!4},
+    backgroundcolor=\color{red!6},
     frame=lines,
     basicstyle=\footnotesize\ttfamily,#1}}{}
 %%% 

examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex

@@ -47,7 +47,7 @@
 }
 \lstdefinestyle{displayltx}{style=ltx,
                 basicstyle=\ttfamily\footnotesize,
-                backgroundcolor=\color{yellow!4}, frame=lines}%
+                backgroundcolor=\color{yellow!7}, frame=lines}%
 
 \lstnewenvironment{ltx}[1][]{\lstset{style=displayltx, #1}}{}
 \def\inlineltx{\lstinline[style=ltx, breaklines=true,columns=fullflexible]}
@@ -77,7 +77,7 @@
 }
 \lstdefinestyle{displaybash}{style=bash,
                 basicstyle=\ttfamily\footnotesize,
-                backgroundcolor=\color{black!2}, frame=lines}%
+                backgroundcolor=\color{black!5}, frame=lines}%
 
 \lstnewenvironment{bash}[1][]{\lstset{style=displaybash, #1}}{}
 \def\inlinebash{\lstinline[style=bash, breaklines=true,columns=fullflexible]}
@@ -101,6 +101,7 @@ Copyright \copyright{} 2018--2019 Universit\'e Paris-Saclay, France\\
 Copyright \copyright{} 2019\phantom{--2019} University of Exeter, UK\\
 All rights reserved.
 
+\begin{small}
 Redistribution and use in source and binary forms, with or without
 modification, are permitted provided that the following conditions are
 met:
@@ -112,6 +113,7 @@ met:
         disclaimer in the documentation and/or other materials provided
        with the distribution.
 \end{itemize}
+\end{small}\begin{small}
 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS ``AS IS''
 AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE 
 IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE 
@@ -122,12 +124,21 @@ SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
 OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+\end{small}
+
 \medskip
-SPDX-License-Identifier: BSD-2-Clause
+\textbf{SPDX-License-Identifier:} BSD-2-Clause
 }
 
-\lowertitleback{\textbf{Note:}\\
-  This manual describes \isadof version 1.0/2019. 
+\lowertitleback{
+{\large This manual describes \isadof version Unreleased/2019.}
+
+\paragraph*{Contributors.} We would like to thank the following contributors to \isadof 
+(in alphabetical order): Idir Ait-Sadoune, Paolo Crisafulli, and Chantal Keller.
+
+\paragraph*{Acknowledgments.} This work has been partially supported by IRT SystemX, Paris-Saclay, 
+France, and therefore granted with public funds of the Program ``Investissements d'Avenir.''
+
 }