Merge branch 'main' into Isabelle_dev

.woodpecker/README.md

@@ -15,4 +15,6 @@ It may also contain additional tools and script that are useful for preparing a
 * pdflatex
   * [browser_info](https://artifacts.logicalhacking.com/ci/Isabelle_DOF/Isabelle_DOF/main/latest/pdflatex/browser_info/Unsorted/)
   * [aux files](https://artifacts.logicalhacking.com/ci/Isabelle_DOF/Isabelle_DOF/main/latest/pdflatex/)
+<!--
 * [Isabelle_DOF-Unreleased_Isabelle2022.tar.xz](https://artifacts.logicalhacking.com/ci/Isabelle_DOF/Isabelle_DOF/main/latest/Isabelle_DOF-Unreleased_Isabelle2022.tar.xz)
+-->

.woodpecker/build.yml

@@ -9,9 +9,6 @@ pipeline:
       - mkdir -p $ISABELLE_HOME_USER/etc
       - echo "ISABELLE_PDFLATEX=\"$LATEX --file-line-error\"" >> $ISABELLE_HOME_USER/etc/settings
       - isabelle build -v -x HOL-Proofs -x Isabelle_DOF-Proofs -D . -o browser_info
-      - isabelle components -u .
-      - isabelle dof_mkroot -q DOF_test
-      - isabelle build -D DOF_test
       - cp -r $ISABELLE_HOME_USER/browser_info $ARTIFACT_DIR
       - cd $ARTIFACT_DIR
       - cd ../..
@@ -23,7 +20,7 @@ pipeline:
       - mkdir -p $ARTIFACT_DIR
       - export ISABELLE_VERSION=`isabelle version`
       - ./.woodpecker/mk_release -d
-      - cp Isabelle_DOF-Unreleased_$ISABELLE_VERSION.tar.xz $ARTIFACT_DIR/../
+      - true || cp Isabelle_DOF-Unreleased_$ISABELLE_VERSION.tar.xz $ARTIFACT_DIR/../
     when:
       matrix:
         LATEX: lualatex

.woodpecker/mk_release

@@ -143,6 +143,7 @@ publish_archive()
     ssh 0x5f.org chmod go+u-w -R www/$DOF_ARTIFACT_HOST/htdocs/$DOF_ARTIFACT_DIR
 }
 
+exit 0
 
 ISABELLE=`which isabelle`
 USE_TAG="false"

Isabelle_DOF-Example-Scholarly_Paper/ROOT

@@ -1,5 +1,5 @@
 session "Isabelle_DOF-Example-Scholarly_Paper" (AFP) = "Isabelle_DOF" + 
-  options [document = pdf, document_output = "output", document_build = dof, quick_and_dirty = true]
+  options [document = pdf, document_output = "output", document_build = dof]
   theories
     IsaDofApplications
   document_files

Isabelle_DOF-Unit-Tests/AssnsLemmaThmEtc.thy

@@ -16,6 +16,7 @@ theory
 imports 
   "Isabelle_DOF-Ontologies.Conceptual"  
   "Isabelle_DOF.scholarly_paper"
+  "Isabelle_DOF-Unit-Tests_document"
 begin
 
 section\<open>Elementary Creation of Doc-items and Access of their Attibutes\<close>

Isabelle_DOF-Unit-Tests/Attributes.thy

@@ -13,7 +13,8 @@
 
 theory 
   Attributes
-imports 
+  imports 
+  "Isabelle_DOF-Unit-Tests_document"
   "Isabelle_DOF-Ontologies.Conceptual"
 begin
 
@@ -210,7 +211,7 @@ open_monitor*[figs4::figure_group,
               caption="''Sample ''"]
 ML\<open>val monitor_infos = DOF_core.get_monitor_infos \<^context>\<close>
 
-text*[testRejected1::figure_group, caption="''figures/A.png''"]
+text*[testRejected1::figure_group, caption="''document/figures/A.png''"]
        \<open> The A train \ldots \<close>
 
 figure*[fig_E::figure,
@@ -219,7 +220,7 @@ figure*[fig_E::figure,
        \<open> The E train \ldots \<close>
 close_monitor*[figs4]
 close_monitor*[figs2]
-text*[testRejected2::figure_group, caption="''figures/A.png''"]
+text*[testRejected2::figure_group, caption="''document/figures/A.png''"]
        \<open> The A train \ldots \<close>
 
 close_monitor*[figs1]  
@@ -231,7 +232,7 @@ ML  \<open>@{trace_attribute figs1}\<close>
 text\<open>Resulting trace of figs as text antiquotation:\<close>
 text\<open>@{trace_attribute figs1}\<close>
 
-text\<open>Test trace_attribute term antiquotation:\<close>
+text\<open>Test trace\_attribute term antiquotation:\<close>
 
 term*\<open>map snd @{trace-attribute \<open>figs1\<close>}\<close>
 value*\<open>map snd @{trace-attribute \<open>figs1\<close>}\<close>

Isabelle_DOF-Unit-Tests/Cenelec_Test.thy

@@ -1,7 +1,8 @@
 theory 
   Cenelec_Test
 imports 
-  "Isabelle_DOF.CENELEC_50128"
+  "Isabelle_DOF-Unit-Tests_document"
+  "Isabelle_DOF-Ontologies.CENELEC_50128"
 begin
 
 declare[[strict_monitor_checking = true]]
@@ -66,3 +67,4 @@ declare[[strict_monitor_checking = true]]
 declare[[invariants_checking = true]]
 declare[[invariants_checking_with_tactics = true]]
 
+end 

Isabelle_DOF-Unit-Tests/Concept_Example.thy

@@ -15,7 +15,8 @@ chapter\<open>Setting and modifying attributes of doc-items\<close>
 
 theory 
   Concept_Example
-imports 
+  imports 
+  "Isabelle_DOF-Unit-Tests_document"
   "Isabelle_DOF-Ontologies.Conceptual" (* we use the generic "Conceptual" ontology *)
 begin
 
@@ -42,7 +43,7 @@ text\<open>Note that both the notations @{term "''beta''"} and @{term "\<open>be
 the former is a more ancient format only supporting pure ascii, while the latter also supports
 fancy unicode such as: @{term "\<open>\<beta>\<^sub>i''\<close>"} \<close>
 
-text*[f::F] \<open> Lectus accumsan velit ultrices, ... }\<close>
+text*[f::F] \<open> Lectus accumsan velit ultrices, ... \<close>
   
 theorem some_proof : "True" by simp
 

Isabelle_DOF-Unit-Tests/Concept_Example_Low_Level_Invariant.thy

@@ -15,7 +15,8 @@ chapter\<open>Setting and modifying attributes of doc-items\<close>
 
 theory 
   Concept_Example_Low_Level_Invariant
-imports 
+  imports 
+  "Isabelle_DOF-Unit-Tests_document"
   "Isabelle_DOF-Ontologies.Conceptual" (* we use the generic "Conceptual" ontology *)
 begin
 
@@ -118,10 +119,10 @@ text*[d1::E, a1 = "X3"]          \<open> ... phasellus amet id massa nunc, pede
     
 text*[c2:: C, x = "''delta''"]   \<open> ... in ut tortor eleifend augue pretium consectetuer...  \<close>
 
-subsection*[f::E]                \<open> Lectus accumsan velit ultrices, ... }\<close>
+subsection*[f::E]                \<open> Lectus accumsan velit ultrices, ... \<close>
 
 (*
-section*[f2::E]                  \<open> Lectus accumsan velit ultrices, ... }\<close>
+section*[f2::E]                  \<open> Lectus accumsan velit ultrices, ... \<close>
 *)
 
 ML\<open>val ctxt = @{context}

Isabelle_DOF-Unit-Tests/Evaluation.thy

@@ -7,17 +7,21 @@ theory
 imports 
   "Isabelle_DOF-Unit-Tests.TermAntiquotations"
   "Isabelle_DOF-Unit-Tests.High_Level_Syntax_Invariants"
+
 begin
 
+(*
 section\<open>\<^theory_text>\<open>ML*\<close>-Annotated SML-commands\<close>
-ML*[the_function::B,x=\<open>\<open>dfg\<close>\<close>]\<open>fun fac x = if x = 0 then 1 else x * fac(x-1);
+
-                               val t = \<^value_>\<open>x @{B \<open>the_function\<close>}\<close>\<close>
+ML*[thefunction::B,x=\<open>\<open>dfg\<close>\<close>]\<open>fun fac x = if x = 0 then 1 else x * fac(x-1);
+                               val t = \<^value_>\<open>x @{B \<open>thefunction\<close>}\<close>\<close>
 ML\<open>fac 5; t\<close> \<comment> \<open>this is a test that ML* is actually evaluated and the 
                  resulting toplevel state is preserved.\<close>
+text-macro*[the::C]\<open> @{B [display] "thefunction"} \<close>
 
-text-macro*[the::C]\<open> @{B [display] "the_function"} \<close>
+text\<open>... and here we reference @{B [display] \<open>thefunction\<close>}.\<close>
 
-text\<open>... and here we reference @{B [display] \<open>the_function\<close>}.\<close>
+*)
 
 section\<open>\<^theory_text>\<open>value*\<close>-Annotated evaluation-commands\<close>
 
@@ -35,13 +39,13 @@ Some built-ins remain as unspecified constants:
 \<^item> the termrepr TA is left as unspecified constant for now.
    A major refactoring of code should be done to enable
   referential equivalence for termrepr, by changing the dependency
-  between the Isa_DOF theory and the Assert theory.
+  between the Isa-DOF theory and the Assert theory.
-  The assert_cmd function in Assert should use the value* command
+  The assert-cmd function in Assert should use the value* command
   functions, which make the elaboration of the term
   referenced by the TA before passing it to the evaluator
 
 We also have the possibility to make some requests on classes instances, i.e. on docitems
-by specifying the doc_class.
+by specifying the doc class.
 The TA denotes the HOL list of the values of the instances.
 The value of an instance is the record of every attributes of the instance.
 This way, we can use the usual functions on lists to make our request.
@@ -101,7 +105,7 @@ text\<open>Some terms can be validated, i.e. the term will be checked,
 and the existence of every object referenced by a TA will be checked,
 and can be evaluated by using referential equivalence.
 The existence of the instance @{docitem \<open>xcv4\<close>} can be validated,
-and the fact that it is an instance of the class @{doc_class F} } will be checked:\<close>
+and the fact that it is an instance of the class @{doc_class F} will be checked:\<close>
 term*\<open>@{F \<open>xcv4\<close>}\<close>
 
 text\<open>We can also evaluate the instance @{docitem \<open>xcv4\<close>}.
@@ -112,12 +116,13 @@ used in the \<open>b\<close> attribute will be checked, and the type of these cl
 \<close>
 value* \<open>@{F \<open>xcv4\<close>}\<close>
 
+(*
 text\<open>If we want the classes to be checked,
 we can use the TA which will also check the type of the instances.
 The instance @{A \<open>xcv3\<close>} is of type @{typ "A"} and the instance @{C \<open>xcv2\<close>} is of type @{typ "C"}:
 \<close>
 update_instance*[xcv4::F, b+="{(@{A ''xcv3''},@{C ''xcv2''})}"]
-
+*)
 text\<open>Using a TA in terms is possible, and the term is evaluated:\<close>
 value*\<open>[@{thm \<open>HOL.refl\<close>}, @{thm \<open>HOL.refl\<close>}]\<close>
 value*\<open>@{thm ''HOL.refl''} = @{thm (''HOL.refl'')}\<close>
@@ -184,12 +189,12 @@ It uses the same implementation as the \<^emph>\<open>value*\<close>-command and
 
 text\<open>Using the ontology defined in \<^theory>\<open>Isabelle_DOF-Unit-Tests.High_Level_Syntax_Invariants\<close>
 we can check logical statements:\<close>
-
+(*
 term*\<open>authored_by @{introduction \<open>introduction2\<close>} = authored_by @{introduction \<open>introduction3\<close>}\<close>
 assert*\<open>authored_by @{introduction \<open>introduction2\<close>} = authored_by @{introduction \<open>introduction3\<close>}\<close>
 assert*\<open>\<not>(authored_by @{introduction \<open>introduction2\<close>}
           = authored_by @{introduction \<open>introduction4\<close>})\<close>
-
+*)
 text\<open>Assertions must be boolean expressions, so the following assertion triggers an error:\<close>
 (* Error:
 assert*\<open>@{introduction \<open>introduction2\<close>}\<close>*)
@@ -197,7 +202,7 @@ assert*\<open>@{introduction \<open>introduction2\<close>}\<close>*)
 text\<open>Assertions must be true, hence the error:\<close>
 (* Error:
 assert*\<open>{@{author \<open>curry\<close>}} = {@{author \<open>church\<close>}}\<close>*)
-
+(*
 term*\<open>property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
 assert*[assertionA::A]\<open>\<not> property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
 
@@ -205,9 +210,11 @@ text-macro*[assertionAA::A]\<open>@{A [display] "assertionA"}\<close>
 text\<open>... and here we reference @{A [display] \<open>assertionA\<close>}.\<close>
 
 assert*\<open>evidence @{result \<open>resultProof\<close>} = evidence @{result \<open>resultProof2\<close>}\<close>
-
+*)
 text\<open>The optional evaluator of \<open>value*\<close> and \<open>assert*\<close> must be specified after the meta arguments:\<close>
 value* [optional_test_A::A, x=6] [nbe] \<open>filter (\<lambda>\<sigma>. A.x \<sigma> > 5) @{A-instances}\<close>
+(*
 assert* [resultProof3::result, evidence = "proof", property="[@{thm \<open>HOL.sym\<close>}]"] [nbe]
         \<open>evidence @{result \<open>resultProof3\<close>} = evidence @{result \<open>resultProof2\<close>}\<close>
+*)
 end

Isabelle_DOF-Unit-Tests/High_Level_Syntax_Invariants.thy

@@ -2,6 +2,8 @@ chapter\<open>High level syntax Invariants\<close>
 
 theory High_Level_Syntax_Invariants
   imports "Isabelle_DOF.Isa_DOF"
+  "Isabelle_DOF-Unit-Tests_document"
+
 begin
 
 text\<open>
@@ -149,14 +151,14 @@ text\<open>The invariants \<^theory_text>\<open>author_finite\<close> and \<^the
   It will enable a basic tactic, using unfold and auto:\<close>
 
 declare[[invariants_checking_with_tactics = true]]
-
+(*
 text*[curry::author, email="\<open>curry@lambda.org\<close>"]\<open>\<close>
 text*[introduction2::introduction, authored_by = "{@{author \<open>church\<close>}}", level = "Some 2"]\<open>\<close>
-(* When not commented, should violated the invariant:
+ When not commented, should violated the invariant:
 update_instance*[introduction2::introduction
                   , authored_by := "{@{author \<open>church\<close>}}"
                   , level := "Some 1"]
-*)
+
 
 text*[introduction3::introduction, authored_by = "{@{author \<open>church\<close>}}", level = "Some 2"]\<open>\<close>
 text*[introduction4::introduction, authored_by = "{@{author \<open>curry\<close>}}", level = "Some 4"]\<open>\<close>
@@ -181,5 +183,5 @@ value*\<open>evidence @{result \<open>resultProof\<close>} = evidence @{result \
 declare[[invariants_checking_with_tactics = false]]
 
 declare[[invariants_strict_checking = false]]
-
+*)
 end

Isabelle_DOF-Unit-Tests/Isabelle2022.thy

@@ -1,221 +0,0 @@
-chapter \<open>Notes on Isabelle/DOF for Isabelle2022\<close>
-
-theory "Isabelle2022"
-  imports Main
-begin
-
-section \<open>Isabelle/DOF component setup\<close>
-
-subsection \<open>Terminology\<close>
-
-text \<open>
-  \<^item> The concept of \<^emph>\<open>Isabelle system component\<close> is explained in \<^doc>\<open>system\<close>
-  section 1.1.1; see also \<^tool>\<open>components\<close> explained in section 7.3.
-
-    For example:
-
-      \<^verbatim>\<open>isabelle components -l\<close>
-
-\<close>
-
-
-subsection \<open>Isabelle/DOF as component\<close>
-
-text \<open>
-  Formal Isabelle/DOF component setup happens here:
-
-  \<^item> \<^path>\<open>$ISABELLE_HOME_USER/etc/components\<close>
-
-    \<^item> A suitable directory entry in the file registers our component to
-    existing Isabelle installation; it also activates the session
-    directory tree starting at \<^file>\<open>$ISABELLE_DOF_HOME/ROOTS\<close>.
-
-    \<^item> Alternative: use \<^path>\<open>$ISABELLE_HOME/Admin/build_release\<close> with
-    option \<^verbatim>\<open>-c\<close> to produce a derived Isabelle distribution that bundles
-    our component for end-users (maybe even with AFP entries).
-
-  \<^item> \<^file>\<open>$ISABELLE_DOF_HOME/etc/settings\<close>
-
-    \<^item> This provides a pervasive Bash process environment (variables,
-    shell functions etc.). It may refer to \<^verbatim>\<open>$COMPONENT\<close> for the
-    component root, e.g. to retain it in variable \<^dir>\<open>$ISABELLE_DOF_HOME\<close>.
-
-    \<^item> Historically, it used to be the main configuration area, but today
-    we see more and more alternatives, e.g. system options or services in
-    Isabelle/Scala (see below).
-
-  \<^item> \<^path>\<open>$ISABELLE_DOF_HOME/etc/options\<close> should not be used for regular
-    Isabelle/DOF applications: thus it works properly within Isabelle/AFP,
-    where the component context is missing.
-\<close>
-
-
-section \<open>Document preparation in Isabelle/ML\<close>
-
-subsection \<open>Session presentation hook\<close>
-
-text \<open>
-  \<^ML>\<open>Build.add_hook\<close> allows to install a global session presentation
-  hook. It is used e.g. in Isabelle/Mirabelle to analyze all loaded
-  theories via Sledgehammer and other tools. Isabelle/DOF could use it to
-  "wrap-up" the whole session, to check if all document constraints hold
-  (cf. "monitors").
-\<close>
-
-
-subsection \<open>Theory presentation hook\<close>
-
-text \<open>
-  \<^ML>\<open>Thy_Info.add_presentation\<close> installs a hook to be invoked at the
-  end of successful loading of theories; the provided context
-  \<^ML_type>\<open>Thy_Info.presentation_context\<close> provides access to
-  \<^ML_type>\<open>Options.T\<close> and \<^ML_type>\<open>Document_Output.segment\<close> with
-  command-spans and semantic states.
-
-  An example is regular Latex output in
-  \<^file>\<open>$ISABELLE_HOME/src/Pure/Thy/thy_info.ML\<close> where \<^ML>\<open>Export.export\<close>
-  is used to produce export artifacts in the session build database, for
-  retrieval via Isabelle/Scala.
-\<close>
-
-
-subsection \<open>Document commands\<close>
-
-text \<open>
-  Isar toplevel commands now support a uniform concept for
-  \<^ML_type>\<open>Toplevel.presentation\<close>, e.g. see
-  \<^ML>\<open>Toplevel.present\<close> and \<^ML>\<open>Toplevel.present_local_theory\<close>.
-\<close>
-
-
-subsection \<open>Document content\<close>
-
-text \<open>
-  XML is now used uniformly (sometimes as inlined YXML). The meaning of
-  markup elements and properties is defined in
-  \<^scala_type>\<open>isabelle.Latex.Output\<close> (or user-defined subclasses).
-\<close>
-
-
-section \<open>Isabelle/Scala services\<close>
-
-subsection \<open>Isabelle/DOF/Scala module\<close>
-
-text \<open>
-  \<^item> \<^file>\<open>$ISABELLE_DOF_HOME/etc/build.props\<close> is the main specification for
-  the Isabelle/DOF/Scala module. It is built on the spot as required, e.g.
-  for \<^verbatim>\<open>isabelle scala\<close> or \<^verbatim>\<open>isabelle jedit\<close>; an alternative is to invoke
-  \<^verbatim>\<open>isabelle scala_build\<close> manually. See also \<^doc>\<open>system\<close>, chapter 5,
-  especially section 5.2.
-
-  \<^item> \<^verbatim>\<open>isabelle scala_project\<close> helps to develop Isabelle/Scala tools with
-  proper IDE support, notably IntelliJ IDEA: the generated project uses
-  Maven. See also \<^doc>\<open>system\<close>, section 5.2.3.
-
-  \<^item> Command-line tools should be always implemented in Scala; old-fashioned
-  shell scripts are no longer required (and more difficult to implement
-  properly). Only a few low-level tools are outside the Scala environment,
-  e.g. \<^verbatim>\<open>isabelle getenv\<close>. Add-on components should always use a name
-  prefix for their tools, e.g. \<^verbatim>\<open>isabelle dof_mkroot\<close> as defined in
-  \<^file>\<open>$ISABELLE_DOF_HOME/src/scala/dof_mkroot.scala\<close>.
-\<close>
-
-
-subsection \<open>Document preparation\<close>
-
-text \<open>
-  \<^item> \<^scala_type>\<open>isabelle.Document_Build.Engine\<close> is the main entry-point
-  for user-defined document preparation; existing templates and examples
-  are defined in the same module \<^file>\<open>~~/src/Pure/Thy/document_build.scala\<close>.
-  There are two stages:
-
-    \<^enum> \<^verbatim>\<open>prepare_directory\<close>: populate the document output directory (e.g.
-    copy static document files, collect generated document sources from the
-    session build database).
-
-    \<^enum> \<^verbatim>\<open>build_document\<close>: produce the final PDF within the document output
-    directory (e.g. via standard LaTeX tools).
-
-  See also \<^system_option>\<open>document_build\<close> as explained in \<^doc>\<open>system\<close>,
-  section 3.3.
-\<close>
-
-
-section \<open>Miscellaneous NEWS and Notes\<close>
-
-text \<open>
-  \<^item> Document preparation: there are many new options etc. that might help
-    to fine-tune DOF output, e.g. \<^system_option>\<open>document_heading_prefix\<close>.
-
-  \<^item> ML: \<^ML>\<open>Thm.instantiate\<close> and related operations now use explicit
-    abstract types for the instantiate, see \<^file>\<open>~~/src/Pure/term_items.ML\<close>
-
-  \<^item> ML: new antiquotation "instantiate" allows to instantiate formal
-    entities (types, terms, theorems) with values given ML. For example:
-
-    \<^ML>\<open>fn (A, B) =>
-        \<^instantiate>\<open>'a = A and 'b = B in typ \<open>('a \<times> 'b) list\<close>\<close>\<close>
-
-    \<^ML>\<open>fn A =>
-        \<^instantiate>\<open>'a = A in
-          lemma (schematic) \<open>x = y \<Longrightarrow> y = x\<close> for x y :: 'a by simp\<close>\<close>
-
-  \<^item> ML: new antiquotations for type constructors and term constants. For
-  example:
-
-    \<^ML>\<open>\<^Type>\<open>nat\<close>\<close>
-    \<^ML>\<open>\<^Type>\<open>prod \<^Type>\<open>int\<close> \<^Type>\<open>int\<close>\<close>\<close>
-
-    \<^ML>\<open>fn (A, B) => \<^Type>\<open>fun A B\<close>\<close>
-    \<^ML>\<open>\<^Type_fn>\<open>fun A B => \<open>(A, B)\<close>\<close>\<close>
-
-    \<^ML>\<open>fn (A, B) => \<^Const>\<open>conj for A B\<close>\<close>
-    \<^ML>\<open>\<^Const_fn>\<open>conj for A B => \<open>(A, B)\<close>\<close>\<close>
-
-    \<^ML>\<open>fn t =>
-      case t of
-        \<^Const_>\<open>plus T for x y\<close> => ("+", T, x, y)
-      | \<^Const_>\<open>minus T for x y\<close> => ("-", T, x, y)
-      | \<^Const_>\<open>times T for x y\<close> => ("*", T, x, y)\<close>
-
-    Note: do not use unchecked things like
-    \<^ML>\<open>Const ("List.list.Nil", Type ("Nat.nat", []))\<close>
-
-  \<^item> ML: antiquotations "try" and "can" operate directly on the given ML
-    expression, in contrast to functions "try" and "can" that modify
-    application of a function.
-
-    Note: instead of semantically ill-defined "handle _ => ...", use
-    something like this:
-
-    \<^ML>\<open>
-      fn (x, y) =>
-        (case \<^try>\<open>x div y\<close> of
-          SOME z => z
-        | NONE => 0)
-    \<close>
-
-    \<^ML>\<open>
-      fn (x, y) => \<^try>\<open>x div y\<close> |> the_default 0
-    \<close>
-\<close>
-
-text \<open>Adhoc examples:\<close>
-
-ML \<open>
-  fun mk_plus x y = \<^Const>\<open>plus \<^Type>\<open>nat\<close> for x y\<close>;
-
-  fn \<^Const_>\<open>plus \<^Type>\<open>nat\<close> for \<^Const_>\<open>Groups.zero \<^Type>\<open>nat\<close>\<close> y\<close> => y;
-\<close>
-
-ML \<open>
-  fn (A, B) =>
-    \<^instantiate>\<open>A and B in term \<open>A \<and> B \<longrightarrow> B \<and> A\<close>\<close>;
-
-  fn (A, B) =>
-    \<^instantiate>\<open>A and B in lemma \<open>A \<and> B \<longrightarrow> B \<and> A\<close> by simp\<close>;
-\<close>
-
-end
-
-(* :maxLineLen=75: *)

Isabelle_DOF-Unit-Tests/Isabelle_DOF-Unit-Tests_document.thy

@@ -0,0 +1,20 @@
+(*<*)
+theory "Isabelle_DOF-Unit-Tests_document"
+  imports
+    "Isabelle_DOF.technical_report"
+    "Isabelle_DOF-Ontologies.CENELEC_50128"
+  
+begin
+
+use_template "scrreprt-modern"
+use_ontology "technical_report" and "Isabelle_DOF-Ontologies.CENELEC_50128"
+
+(*>*)
+(* BUG: Invariant checking should not go across sessions boundaries.
+
+title*[title::title]         \<open>Isabelle/DOF\<close>
+subtitle*[subtitle::subtitle]\<open>Unit Tests\<close>
+*)
+(*<*)
+end
+(*>*)

Isabelle_DOF-Unit-Tests/Ontology_Matching_Example.thy

@@ -2,6 +2,8 @@ chapter\<open>Ontologys Mathing\<close>
 
 theory Ontology_Matching_Example
   imports "Isabelle_DOF.Isa_DOF"
+  "Isabelle_DOF-Unit-Tests_document"
+
 begin
 
 text\<open>Using HOL, we can define a mapping between two ontologies.

Isabelle_DOF-Unit-Tests/OutOfOrderPresntn.thy

@@ -14,7 +14,8 @@
 theory 
   OutOfOrderPresntn
 imports 
-  "Isabelle_DOF.Conceptual"
+  "Isabelle_DOF-Unit-Tests_document"
+  "Isabelle_DOF-Ontologies.Conceptual"
 keywords "text-" "textN"    :: document_body  
     and  "Figure*"          :: document_body 
 
@@ -129,6 +130,7 @@ val _ =
 \<close>
 
 ML\<open>open Bytes\<close>
+(*
 text\<open>And here a tex - text macro.\<close>
 text\<open>Pythons ReStructuredText (RST). 
      @{url \<open>https://de.wikipedia.org/wiki/ReStructuredText\<close>}. Tool: Sphinx.
@@ -137,9 +139,9 @@ text\<open>Pythons ReStructuredText (RST).
 text*[aaaa::B]\<open>dfg @{thm [display] refl}\<close>
                             
 text-[dfgdfg::B]
-\<open> Lorem ipsum ...  @{thm [display] refl} _ Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close>  \<close>
+\<open> Lorem ipsum ...  @{thm [display] refl}  Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close>  \<close>
 
-textN\<open> Lorem ipsum ...  @{thm [display] refl} _ Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close>  \<close>
+textN\<open> Lorem ipsum ...  @{thm [display] refl}  Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close>  \<close>
 
 text-[asd::B]
 \<open>... and here is its application macro expansion: 
@@ -147,7 +149,7 @@ text-[asd::B]
      \textbf{TEST}
      @{cartouche [display] 
          \<open>text*[dfgdfg::B]
-           \<open> Lorem ipsum ...  @{thm refl} _ Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close>  \<close>
+           \<open> Lorem ipsum ...  @{thm refl} Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close>  \<close>
           \<close>}
 \<close>
 
@@ -156,7 +158,7 @@ textN\<open>... and here is its application macro expansion:
      \textbf{TEST}
      @{cartouche [display] 
          \<open>text*[dfgdfg::B]
-           \<open> Lorem ipsum ...  @{thm refl} _ Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close>  \<close>
+           \<open> Lorem ipsum ...  @{thm refl}  Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close>  \<close>
           \<close>}\<close>
 
 textN\<open> \<^theory_text>\<open>definition df = ...  
@@ -167,12 +169,12 @@ textN\<open> \<^theory_text>\<open>definition df = ...
        @{ML_text [display] \<open> val x = ...  
                            \<close>}
 
-       @{verbatim [display] \<open> Lorem ipsum ...  @{thm refl} _ 
+       @{verbatim [display] \<open> Lorem ipsum ...  @{thm refl} 
                               Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close> \<close>}
        @{theory_text [display] \<open>definition df = ... \<lambda>x.  
                                \<close>}
        @{cartouche [display]   \<open> @{figure "cfgdfg"}\<close>} \<close>
-
+*)
 (*<*)
 text\<open>Final Status:\<close>
 print_doc_items
@@ -497,7 +499,7 @@ val _ =
 
 
 \<close>
-
+(*
 Figure*[fff::figure,src="\<open>this is a side-by-side\<close>"]
    \<open>@{figure_content [width=40, scale=35, caption="This is a test"] "ROOT"}\<close> 
    \<open> \<^doof> \<^LATEX> \<close>  
@@ -505,7 +507,7 @@ Figure*[fff::figure,src="\<open>this is a side-by-side\<close>"]
      @{ML        [display]   \<open> let val x = 3 + 4 in true end\<close>}
      @{cartouche [display]   \<open> @{figure "cfgdfg"}\<close>}
    \<close>  
-
+*)
 
 
 Figure*[ffff::figure2, caption="\<open>this is another 2 side-by-side\<close>"]

Isabelle_DOF-Unit-Tests/ROOT

@@ -1,5 +1,5 @@
 session "Isabelle_DOF-Unit-Tests" = "Isabelle_DOF-Ontologies" + 
-  options [document = false]
+  options [document = pdf, document_output = "output", document_build = dof]
   theories
     "AssnsLemmaThmEtc" 
     "Concept_Example_Low_Level_Invariant"
@@ -9,7 +9,9 @@ session "Isabelle_DOF-Unit-Tests" = "Isabelle_DOF-Ontologies" +
     "Evaluation"
     "High_Level_Syntax_Invariants"
     "Ontology_Matching_Example"
-  theories [condition = ISABELLE_DOF_HOME]
+    "Cenelec_Test"
-    "Isabelle2022"
+    "OutOfOrderPresntn"
   document_files
     "root.bib"
+    "figures/A.png"
+    "figures/B.png"

Isabelle_DOF-Unit-Tests/TermAntiquotations.thy

@@ -20,6 +20,7 @@ For historical reasons, \<^emph>\<open>term antiquotations\<close> are called th
 theory 
   TermAntiquotations
 imports 
+  "Isabelle_DOF-Unit-Tests_document"
   "Isabelle_DOF-Ontologies.Conceptual"
 begin
 
@@ -40,7 +41,7 @@ ODL on a paradigmatical example.
 \<close>
 
 
-text\<open>Voila the content of the Isabelle_DOF environment so far:\<close>
+text\<open>Voila the content of the Isabelle/DOF environment so far:\<close>
 ML\<open>
 val x = DOF_core.get_instances \<^context>
 val isa_transformer_tab = DOF_core.get_isa_transformers \<^context>
@@ -61,7 +62,7 @@ text*[xcv1::A, x=5]\<open>Lorem ipsum ...\<close>
 text*[xcv3::A, x=7]\<open>Lorem ipsum ...\<close>
 
 text\<open>Example for a meta-attribute of ODL-type @{typ "typ"} with an appropriate ISA for the
-     theorem @{thm "refl"}}\<close>
+     theorem @{thm "refl"}\<close>
 text*[xcv2::C, g="@{thm ''HOL.refl''}"]\<open>Lorem ipsum ...\<close>
 
 text\<open>A warning about the usage of the \<open>docitem\<close> TA:
@@ -107,12 +108,12 @@ 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>
 
-text\<open>We declare a new text element. Note that the class name contains an underscore "_".\<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>
 
 text\<open>Unfortunately due to different lexical conventions for constant symbols and mixfix symbols
      this term antiquotation has to be denoted like this: @{term_ \<open>@{text-element \<open>te\<close>}\<close>}.
-     We need to substitute an hyphen "-" for the underscore "_".\<close>
+     We need to substitute an hyphen "-" for the underscore "\_".\<close>
 term*\<open>@{text-element \<open>te\<close>}\<close>
 
 text\<open>Terms containing term antiquotations can be checked and evaluated

Isabelle_DOF/etc/build.props

@@ -5,9 +5,6 @@ requirements = \
   env:ISABELLE_SCALA_JAR
 sources = \
   scala/dof.scala \
-  scala/dof_document_build.scala \
+  scala/dof_document_build.scala
-  scala/dof_mkroot.scala \
-  scala/dof_tools.scala
 services = \
-  isabelle.dof.DOF_Tools \
   isabelle.dof.DOF_Document_Build$Engine

Isabelle_DOF/scala/dof_mkroot.scala

@@ -1,199 +0,0 @@
-/*
- * Copyright (c)
- *               2021-2022 The University of Exeter.
- *               2021-2022 The University of Paris-Saclay.
- *
- * 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
- */
-
-
-/*** create session root directory for Isabelle/DOF ***/
-
-package isabelle.dof
-
-import isabelle._
-
-
-object DOF_Mkroot
-{
-  /** mkroot **/
-
-  val default_ontologies: List[String] = List("technical_report", "scholarly_paper")
-  val default_template = "scrreprt-modern"
-
-  def mkroot(
-    session_name: String = "",
-    session_dir: Path = Path.current,
-    init_repos: Boolean = false,
-    ontologies: List[String] = default_ontologies,
-    template: String = default_template,
-    quiet: Boolean = false,
-    progress: Progress = new Progress): Unit =
-  {
-    Isabelle_System.make_directory(session_dir)
-
-    val name = proper_string(session_name) getOrElse session_dir.absolute_file.getName
-
-    val root_path = session_dir + Sessions.ROOT
-    if (root_path.file.exists) error("Cannot overwrite existing " + root_path)
-
-    val document_path = session_dir + Path.explode("document")
-    if (document_path.file.exists) error("Cannot overwrite existing " + document_path)
-
-    progress.echo(
-      (if (quiet) "" else "\n") +
-      "Initializing session " + quote(name) + " in " + session_dir.absolute)
-
-
-    /* ROOT */
-
-    progress.echo_if(!quiet, "  creating " + root_path)
-
-    File.write(root_path,
-      "session " + Mkroot.root_name(name) + " = " + Mkroot.root_name(DOF.session) + """ +
-  options [document = pdf, document_output = "output", document_build = dof]
-(*theories [document = false]
-    A
-    B*)
-  theories
-    """ + Mkroot.root_name(name) + """
-  document_files
-    "preamble.tex"
-""")
-
-    val thy = session_dir + Path.explode(name + ".thy")
-    progress.echo_if(!quiet, "  creating " + thy)
-    File.write(thy,
-      "theory\n  " + name +
-      "\nimports\n  " + ontologies.map("Isabelle_DOF." + _).mkString("\n  ") +  """
-begin
-
-use_template """ + quote(template) + """
-use_ontology """ + ontologies.map(quote).mkString(" and ") + """
-
-end
-""")
-
-
-    /* preamble */
-
-    val preamble_tex = session_dir + Path.explode("document/preamble.tex")
-    progress.echo_if(!quiet, "  creating " + preamble_tex)
-    Isabelle_System.make_directory(preamble_tex.dir)
-    File.write(preamble_tex,"""%% This is a placeholder for user-specific configuration and packages.""")
-
-
-    /* Mercurial repository */
-
-    if (init_repos) {
-      progress.echo(
-        (if (quiet) "" else "\n") + "Initializing Mercurial repository " + session_dir.absolute)
-
-      val hg = Mercurial.init_repository(session_dir)
-
-      val hg_ignore = session_dir + Path.explode(".hgignore")
-      File.write(hg_ignore,
-"""syntax: glob
-
-*~
-*.marks
-*.orig
-*.rej
-.DS_Store
-.swp
-
-syntax: regexp
-
-^output/
-""")
-
-      hg.add(List(root_path, preamble_tex, hg_ignore))
-    }
-
-
-    /* notes */
-
-    {
-      val print_dir = session_dir.implode
-      progress.echo_if(!quiet, """
-Now use the following command line to build the session:
-
-  isabelle build -D """ +
-        (if (Bash.string(print_dir) == print_dir) print_dir else quote(print_dir)) + "\n")
-    }
-  }
-
-
-
-  /** Isabelle tool wrapper **/
-
-  val isabelle_tool = Isabelle_Tool("dof_mkroot", "create session root directory for Isabelle/DOF",
-    Scala_Project.here, args =>
-  {
-    var init_repos = false
-    var help = false
-    var session_name = ""
-    var ontologies = default_ontologies
-    var template = default_template
-    var quiet = false
-
-    val getopts = Getopts("""
-Usage: isabelle dof_mkroot [OPTIONS] [DIRECTORY]
-
-  Options are:
-    -I           init Mercurial repository and add generated files
-    -h           print help
-    -n NAME      alternative session name (default: directory base name)
-    -o NAMES     list of ontologies, separated by blanks
-                 (default: """ + quote(Word.implode(default_ontologies)) + """)
-    -q           quiet mode: less verbosity
-    -t NAME      template (default: """ + quote(default_template) + """)
-
-  Create session root directory for Isabelle/DOF (default: current directory).
-""",
-      "I" -> (_ => init_repos = true),
-      "h" -> (_ => help = true),
-      "n:" -> (arg => session_name = arg),
-      "o:" -> (arg => ontologies = Word.explode(arg)),
-      "q" -> (_ => quiet = true),
-      "t:" -> (arg => template = arg))
-
-    val more_args = getopts(args)
-    val session_dir =
-      more_args match {
-        case Nil => Path.current
-        case List(dir) => Path.explode(dir)
-        case _ => getopts.usage()
-      }
-
-    if (help) getopts.usage()
-
-    val progress = new Console_Progress
-
-    mkroot(session_name = session_name, session_dir = session_dir,
-      init_repos = init_repos, quiet = quiet, progress = progress,
-      ontologies = ontologies, template = template)
-  })
-}

Isabelle_DOF/scala/dof_tools.scala

@@ -1,42 +0,0 @@
-/*
- * Copyright (c) 
- *               2021-2022 The University of Exeter. 
- *               2021-2022 The University of Paris-Saclay. 
- *
- * 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
- */
-
-
-/*** command-line tools for Isabelle/DOF ***/
- 
-package isabelle.dof
-
-import isabelle._
-
-
-class DOF_Tools extends Isabelle_Scala_Tools(
-  DOF.isabelle_tool,
-  DOF_Mkroot.isabelle_tool,
-)

Isabelle_DOF/thys/Isa_DOF.thy

@@ -3174,18 +3174,14 @@ section \<open>Isabelle/Scala module within session context\<close>
 
 external_file "../etc/build.props"
 external_file "../scala/dof_document_build.scala"
-external_file "../scala/dof_mkroot.scala"
 external_file "../scala/dof.scala"
-external_file "../scala/dof_tools.scala"
 
 scala_build_generated_files
   external_files
     "build.props" (in "../etc")
   and
     "scala/dof_document_build.scala"
-    "scala/dof_mkroot.scala"
+    "scala/dof.scala" (in "../")
-    "scala/dof.scala"
-    "scala/dof_tools.scala" (in "../")
 
 (*
 ML\<open>