added paper frame, small things.

examples/cytology/Cytology.thy

@@ -87,6 +87,4 @@ value \<open>has_nucleus_inv(eucaryotic_cells.make X Y Z Z Z [] 3
 
 
 
-
-
 end

examples/scholarly_paper/2020-iFM-CSP/paper.thy

@@ -1024,6 +1024,10 @@ over finite sub-systems with globally infinite systems in a logically safe way.
 subsection*[bib::bibliography]\<open>References\<close>
 
 close_monitor*[this]
-
+(*
+term\<open>\<longrightarrow>\<close>
+term\<open> demon \<sigma>\<^sub>g\<^sub>l\<^sub>o\<^sub>b\<^sub>a\<^sub>l := \<Sqinter> \<Delta>t \<in> \<real>\<^sub>>\<^sub>0.     ||| i\<in>A. ACTOR i \<sigma>\<^sub>g\<^sub>l\<^sub>o\<^sub>b\<^sub>a\<^sub>l 
+                                   \<lbrakk>S\<rbrakk> sync!\<sigma>\<^sub>g\<^sub>l\<^sub>o\<^sub>b\<^sub>a\<^sub>l\<^sub>' \<longrightarrow> demon \<sigma>\<^sub>g\<^sub>l\<^sub>o\<^sub>b\<^sub>a\<^sub>l\<^sub>'   \<close>
+*)
 end
 (*>*) 

examples/scholarly_paper/2021-ITP-PMTI/ROOT

@@ -0,0 +1,9 @@
+session "2021-ITP-PMTI" = "Isabelle_DOF" +
+  options [document = pdf, document_output = "output"]
+  theories
+    "paper"
+  document_files
+    "isadof.cfg"
+    "root.bib"
+    "preamble.tex"
+    "build"

examples/scholarly_paper/2021-ITP-PMTI/document/build

@@ -0,0 +1,47 @@
+#!/usr/bin/env bash
+# Copyright (c) 2019 University of Exeter
+#               2018-2019 University of Paris-Saclay
+#               2018-2019 The University of Sheffield
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions
+# are met:
+# 1. Redistributions of source code must retain the above copyright
+#    notice, this list of conditions and the following disclaimer.
+# 2. Redistributions in binary form must reproduce the above copyright
+#    notice, this list of conditions and the following disclaimer in
+#    the documentation and/or other materials provided with the
+#    distribution.
+# 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 DISCLAIMED. IN NO EVENT SHALL THE
+# COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
+# INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
+# BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR 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.
+#
+# SPDX-License-Identifier: BSD-2-Clause
+
+set -e
+if [ ! -f $ISABELLE_HOME_USER/DOF/document-template/build_lib.sh ]; then
+    >&2 echo ""
+    >&2 echo "Error: Isabelle/DOF not installed"
+    >&2 echo "====="
+    >&2 echo "This is a Isabelle/DOF project. The document preparation requires"
+    >&2 echo "the Isabelle/DOF framework. Please obtain the framework by cloning"
+    >&2 echo "the Isabelle/DOF git repository, i.e.: "
+    >&2 echo "    git clone https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF"
+    >&2 echo "You can install the framework as follows:"
+    >&2 echo "    cd Isabelle_DOF/document-generator"
+    >&2 echo "    ./install"
+    >&2 echo ""
+    exit 1
+fi
+
+cp $ISABELLE_HOME_USER/DOF/document-template/build_lib.sh .
+source build_lib.sh

examples/scholarly_paper/2021-ITP-PMTI/document/isadof.cfg

@@ -0,0 +1,2 @@
+Template: scrartcl
+Ontology: scholarly_paper

examples/scholarly_paper/2021-ITP-PMTI/document/preamble.tex

@@ -0,0 +1,8 @@
+%% This is a placeholder for user-specific configuration and packages.
+
+\usepackage{stmaryrd}
+
+\title{<TITLE>}
+\author{<AUTHOR>}
+
+

src/DOF/Isa_DOF.thy

@@ -1483,7 +1483,7 @@ in
 end;
 
 fun print_item string_of (modes, arg) = Toplevel.keep (fn state =>
-Print_Mode.with_modes modes (fn () => writeln (string_of state arg)) ());
+Print_Mode.with_modes modes (fn () => writeln (string_of state arg)) ()); 
 
 (*
   We want to have the current position to pass it to transduce_term_global in

src/tests/Attributes.thy

@@ -56,6 +56,20 @@ value [simp] \<open> M.ok
                    (undefined::M)) 
                    ))\<close>
 
+value [simp] \<open> M.ok 
+                   (Conceptual.M.trace_update (\<lambda>x. [])
+                    (Conceptual.M.tag_attribute_update (\<lambda>x. 0)
+                     (Conceptual.M.ok_update (\<lambda>x. ())
+                   (undefined::M)) 
+                   ))\<close>
+value  \<open> M.ok 
+                   (Conceptual.M.trace_update (\<lambda>x. [])
+                    (Conceptual.M.tag_attribute_update (\<lambda>x. 0)
+                     (Conceptual.M.ok_update (\<lambda>x. ())
+                   (AAAA::M)) 
+                   ))\<close>
+
+
 value  \<open> M.ok 
                    (Conceptual.M.trace_update (\<lambda>x. [])
                     (Conceptual.M.tag_attribute_update (\<lambda>x. 0)
@@ -64,18 +78,6 @@ value  \<open> M.ok
                    ))\<close>
 
 
-
-ML\<open>
-fun fac x = if x = 0 then 1 else x * (fac(x -1));
-fac 3;
-\<close>
-
-ML\<open>
-open Thm;
-\<close>
-
-
-
 text\<open>A text item containing standard theorem antiquotations and complex meta-information.\<close>
 (* crashes in batch mode ... 
 text*[dfgdfg::B, Conceptual.B.x ="''f''", y = "[''sdf'']"]\<open> Lorem ipsum ...  @{thm refl} \<close>

src/tests/TermAntiquotations.thy

@@ -95,6 +95,8 @@ text\<open>We can also reference an attribute of the instance.
 Here we reference the attribute r of the class F which has the type @{typ \<open>thm list\<close>}.\<close>
 term*\<open>r @{F \<open>xcv4\<close>}\<close>
 
+term \<open>@{A \<open>xcv2\<close>}\<close>
+
 text\<open>We declare a new text element. Note that the class name contains an underscore "_".\<close>
 text*[te::text_element]\<open>Lorem ipsum...\<close>