Bumped version to 1.3.0.

- added multi-arg syntax (only one arg evaluated so far)
- added figure_content built-in antiquotation
- added new Figure* - multi-arg command.

.config

@@ -1,18 +0,0 @@
-# Isabelle/DOF Version Information
-DOF_VERSION="1.2.0"    # "Unreleased" for development, semantic version for releases 
-DOF_LATEST_VERSION="1.2.0"    
-DOF_LATEST_ISABELLE="Isabelle2021"    
-DOF_LATEST_DOI="10.5281/zenodo.6385695"
-DOF_GENERIC_DOI="10.5281/zenodo.3370482"
-#
-# Isabelle and AFP Configuration
-ISABELLE_VERSION="Isabelle2021: February 2021"
-ISABELLE_URL="https://isabelle.in.tum.de/website-Isabelle2021/"
-AFP_DATE="afp-2021-03-09"
-AFP_URL="https://www.isa-afp.org/release/"$AFP_DATE".tar.gz"
-#
-# Isabelle/DOF Repository Configuration
-DOF_URL="https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF"
-DOF_ARTIFACT_DIR="releases/Isabelle_DOF/Isabelle_DOF"
-DOF_ARTIFACT_HOST="artifacts.logicalhacking.com"
-#

.gitattributes

@@ -1,3 +1,2 @@
-install -crlf
-document-generator/Tools/DOF_mkroot -crlf
-document-generator/document-template/build -crlf
+core.autocrlf false
+core.eol lf

.gitignore

@@ -1,3 +1,4 @@
 output
 .afp
 *~
+*#

.woodpecker/README.md

@@ -9,6 +9,10 @@ It may also contain additional tools and script that are useful for preparing a
 
 ### Latest Build
 
-* [document.pdf](https://artifacts.logicalhacking.com/ci-confidential/Isabelle_DOF/Isabelle_DOF/main/latest/document.pdf)
-* [browser_info](https://artifacts.logicalhacking.com/ci-confidential/Isabelle_DOF/Isabelle_DOF/main/latest/browser_info/Unsorted/Isabelle_DOF/)
-* [aux files](https://artifacts.logicalhacking.com/ci-confidential/Isabelle_DOF/Isabelle_DOF/main/latest/)
+* lualatex
+  * [browser_info](https://artifacts.logicalhacking.com/ci/Isabelle_DOF/Isabelle_DOF/main/latest/lualatex/browser_info/Unsorted/)
+  * [aux files](https://artifacts.logicalhacking.com/ci/Isabelle_DOF/Isabelle_DOF/main/latest/lualatex/)
+* 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_Isabelle2021-1.tar.xz](https://artifacts.logicalhacking.com/ci/Isabelle_DOF/Isabelle_DOF/main/latest/Isabelle_DOF-Unreleased_Isabelle2021-1.tar.xz)

.woodpecker/build.yml

@@ -1,17 +1,31 @@
 pipeline:
   build:
-    image: docker.io/logicalhacking/isabelle2021
+    image: docker.io/logicalhacking/isabelle2021-1
     commands:
-      - export ARTIFACT_DIR=$CI_WORKSPACE/.artifacts/$CI_REPO/$CI_BRANCH/$CI_BUILD_NUMBER/
+      - export ARTIFACT_DIR=$CI_WORKSPACE/.artifacts/$CI_REPO/$CI_BRANCH/$CI_BUILD_NUMBER/$LATEX
       - mkdir -p $ARTIFACT_DIR
       - export `isabelle getenv ISABELLE_HOME_USER`
-      - ./install
+      - mkdir -p $ISABELLE_HOME_USER/etc
+      - echo "ISABELLE_PDFLATEX=\"$LATEX --file-line-error\"" >> $ISABELLE_HOME_USER/etc/settings
+      - isabelle components -u `pwd` 
       - isabelle build -D . -o browser_info
+      - isabelle dof_mkroot DOF_test
+      - isabelle build -D DOF_test
       - cp -r $ISABELLE_HOME_USER/browser_info $ARTIFACT_DIR
-      - cp output/document.pdf $ARTIFACT_DIR
       - cd $ARTIFACT_DIR
-      - cd ..
+      - cd ../..
       - ln -s * latest
+  archive:
+    image: docker.io/logicalhacking/isabelle2021-1
+    commands:
+      - export ARTIFACT_DIR=$CI_WORKSPACE/.artifacts/$CI_REPO/$CI_BRANCH/$CI_BUILD_NUMBER/$LATEX
+      - mkdir -p $ARTIFACT_DIR
+      - export ISABELLE_VERSION=`isabelle version`
+      - ./.woodpecker/mk_release -d
+      - cp Isabelle_DOF-Unreleased_$ISABELLE_VERSION.tar.xz $ARTIFACT_DIR/../
+    when:
+      matrix:
+        LATEX: lualatex
   deploy:
     image: docker.io/drillster/drone-rsync
     settings:
@@ -23,5 +37,18 @@ pipeline:
       key:
         from_secret: artifacts_ssh
       user: artifacts
+  notify:
+    image: drillster/drone-email
+    settings:
+      host: smtp.0x5f.org
+      username: woodpecker
+      password: 
+        from_secret: email
+      from: ci@logicalhacking.com
+    when:
+      status: [ failure ]    
 
-      
+matrix:
+  LATEX:
+  - lualatex      
+  - pdflatex

.woodpecker/isabelle4isadof/Dockerfile

@@ -1,32 +0,0 @@
-# Copyright (c) 2019 Achim D. Brucker
-#
-# All rights reserved.
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions are met:
-#
-# * Redistributions of source code must retain the above copyright notice, this
-#
-# * 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
-
-FROM logicalhacking/lh-docker-isabelle:isabelle2021
-
-WORKDIR /home/isabelle
-COPY thy_output.ML /home/isabelle/Isabelle/src/Pure/Thy
-RUN Isabelle/bin/isabelle build -b Functional-Automata
-

.woodpecker/mk_release

@@ -39,26 +39,18 @@ print_help()
     echo "Run ..."
     echo ""
     echo "  --help, -h                display this help message"
-    echo "  --sign -s                 sign release archive"
+    echo "  --sign, -s                sign release archive"
     echo "                            (default: $SIGN)"
     echo "  --isabelle, -i isabelle   isabelle command used for installation"
     echo "                            (default: $ISABELLE)"
-    echo "  --tag -t tag              use tag for release archive"
+    echo "  --tag tag, -t tag         use tag for release archive"
     echo "                            (default: use master branch)"
-    echo "  --p --publish             publish generated artefact"
-    echo "                            (use master: $PUBLISH)"
+    echo "  --publish, -p             publish generated artefact"
+    echo "                            (default: $PUBLISH)"
+    echo "  --quick-and-dirty, -d     only build required artifacts, no complete test"
+    echo "                            (default: $DIRTY)"
 }
 
-read_config() {
-    if [ ! -f .config ]; then
-        echo "Error: .config not found (not started in the main directory?)!"
-        exit 1
-    else
-        source .config
-    fi
-}
-
-
 check_isabelle_version() {
     ACTUAL_ISABELLE_VERSION=`$ISABELLE version`
     echo "* Checking Isabelle version:"
@@ -80,21 +72,38 @@ clone_repo()
     else
         echo "  * Not tag specified, using master branch"
     fi
-    (cd $ISADOF_WORK_DIR && git show -s --format="COMMIT=%H%nDATE=%cd" --date=short | sed -e 's|-|/|g') >> $ISADOF_WORK_DIR/.config
+    (cd $ISADOF_WORK_DIR && git show -s --format="COMMIT=%H%nDATE=%cd" --date=short | sed -e 's|-|/|g') >> $ISADOF_WORK_DIR/etc/settings
     
 }
 
 build_and_install_manuals()
 {
     echo "* Building manual"
-    ROOTS=$ISABELLE_HOME_USER/ROOTS
-    if [ -f $ROOTS ]; then
-        mv $ROOTS $ROOTS.backup
+
+    if [ "$DIRTY" = "true" ]; then
+        if [ -z ${ARTIFACT_DIR+x} ]; then
+            echo "  * Quick and Dirty Mode (local build)"
+            $ISABELLE build -d . Isabelle_DOF-Manual 2018-cicm-isabelle_dof-applications
+            mkdir -p $ISADOF_WORK_DIR/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/output/
+            cp examples/scholarly_paper/2018-cicm-isabelle_dof-applications/output/document.pdf \
+               $ISADOF_WORK_DIR/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/output/
+            mkdir -p $ISADOF_WORK_DIR/examples/technical_report/Isabelle_DOF-Manual/output/
+            cp examples/technical_report/Isabelle_DOF-Manual/output/document.pdf \
+               $ISADOF_WORK_DIR/examples/technical_report/Isabelle_DOF-Manual/output/;
+        else
+            echo "  * Quick and Dirty Mode (running on CI)"
+            mkdir -p $ISADOF_WORK_DIR/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/output/
+            cp $ARTIFACT_DIR/browser_info/Unsorted/2018-cicm-isabelle_dof-applications/document.pdf \
+               $ISADOF_WORK_DIR/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/output/
+ 
+            mkdir -p $ISADOF_WORK_DIR/examples/technical_report/Isabelle_DOF-Manual/output/
+            cp $ARTIFACT_DIR/browser_info/Unsorted/Isabelle_DOF-Manual/document.pdf \
+               $ISADOF_WORK_DIR/examples/technical_report/Isabelle_DOF-Manual/output/;
+        fi
+    else
+        (cd $ISADOF_WORK_DIR && $ISABELLE env ./install-afp)
+        (cd $ISADOF_WORK_DIR && $ISABELLE build -c -D . )
     fi
-
-    (cd $ISADOF_WORK_DIR && ./install)
-    (cd $ISADOF_WORK_DIR && $ISABELLE build -c -D . )
-
     mkdir -p $ISADOF_WORK_DIR/doc
     echo "Isabelle/DOF Manuals!" > $ISADOF_WORK_DIR/doc/Contents
     
@@ -108,9 +117,7 @@ build_and_install_manuals()
 
     find $ISADOF_WORK_DIR -type d -name "output" -exec rm -rf {} \; &> /dev/null || true
     rm -rf $ISADOF_WORK_DIR/.git* $ISADOF_WORK_DIR/.woodpecker $ISADOF_WORK_DIR/.afp 
-    if [ -f $ROOTS.backup ]; then
-        mv $ROOTS.backup $ROOTS
-    fi
+    
 }
 
 create_archive()
@@ -120,7 +127,6 @@ create_archive()
     (mv $ISADOF_WORK_DIR $ISADOF_DIR)    
     (cd $BUILD_DIR && tar cf $ISADOF_TAR.tar $ISADOF_TAR && xz $ISADOF_DIR.tar)
     mv $BUILD_DIR/$ISADOF_TAR.tar.xz .
-    rm -rf $BUILD_DIR
 }
 
 sign_archive()
@@ -138,11 +144,11 @@ publish_archive()
 }
 
 
-read_config
 ISABELLE=`which isabelle`
 USE_TAG="false"
 SIGN="false"
 PUBLISH="false"
+DIRTY="false"
 BUILD_DIR=`mktemp -d`
 ISADOF_WORK_DIR="$BUILD_DIR/Isabelle_DOF"
 while [ $# -gt 0 ]
@@ -159,6 +165,8 @@ do
             SIGN="true";;
         --publish|-p)
             PUBLISH="true";;
+        --quick-and-dirty|-d)
+            DIRTY="true";;
         --help|-h)
             print_help
             exit 0;;
@@ -171,19 +179,36 @@ done
 
 clone_repo
 
-source $ISADOF_WORK_DIR/.config
+ISADOF_MAIN_DIR=`pwd`
+
+if [ "$DIRTY" = "true" ]; then
+    echo "Running in Quick and Dirty mode!"
+    $ISABELLE components -u $ISADOF_MAIN_DIR
+else
+    $ISABELLE components -x $ISADOF_MAIN_DIR
+    $ISABELLE components -u $ISADOF_WORK_DIR
+fi
+
+VARS=`$ISABELLE getenv ISABELLE_TOOL`
+for i in $VARS; do
+        export "$i"
+done
+
+ISABELLE_VERSION="Isabelle$($ISABELLE_TOOL options -g dof_isabelle)"
+DOF_VERSION="$($ISABELLE_TOOL options -g dof_version)"
+
 ISABELLE_SHORT_VERSION=`echo $ISABELLE_VERSION | sed -e 's/:.*$//'`
 ISADOF_TAR="Isabelle_DOF-"$DOF_VERSION"_"$ISABELLE_SHORT_VERSION
 ISADOF_DIR="$BUILD_DIR/$ISADOF_TAR"
 
 check_isabelle_version
-VARS=`$ISABELLE getenv ISABELLE_HOME_USER`
-for i in $VARS; do
-        export "$i"
-done
-
 build_and_install_manuals
 
+if [ "$DIRTY" != "true" ]; then
+    $ISABELLE components -x $ISADOF_WORK_DIR
+    $ISABELLE components -u $ISADOF_MAIN_DIR
+fi
+
 create_archive
 
 if [ "$SIGN" = "true" ]; then
@@ -194,4 +219,6 @@ if [ "$PUBLISH" = "true" ]; then
     publish_archive
 fi
 
+rm -rf $BUILD_DIR
+
 exit 0 

CHANGELOG.md

@@ -5,9 +5,22 @@ All notable changes to this project will be documented in this file.
 The format is based on [Keep a Changelog](http://keepachangelog.com/en/1.0.0/)
 and this project adheres to [Semantic Versioning](http://semver.org/spec/v2.0.0.html).
 
-## 1.2.0 - 2022-03-26
+## [1.3.0] - 2022-07-08
 
-## 1.1.0 - 2021-03-20
+### Changed
+
+- The project-specific configuration is not part of the `ROOT` file, the formerly 
+  used `isadof.cfg` is obsolete and no longer supported. 
+- Removed explicit use of `document/build` script. Requires removing the `build` script 
+  entry from ROOT files.
+- Isabelle/DOF is now a proper Isabelle component that should be installed using the
+  `isabelle components` command. The installation script is now only a convenient way 
+  of installing the required AFP entries.
+- `mkroot_DOF` has been renamed to `dof_mkroot` (and reimplemented in Scala).
+
+## [1.2.0] - 2022-03-26
+
+## [1.1.0] - 2021-03-20
 
 ### Added
 
@@ -24,4 +37,7 @@ and this project adheres to [Semantic Versioning](http://semver.org/spec/v2.0.0.
 
 - First public release
 
-[Unreleased]: https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF/compare/v1.0.0/Isabelle2019...HEAD
+[Unreleased]: https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF/compare/v1.3.0/Isabelle2021...HEAD
+[v1.3.0]: https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF/compare/v1.2.0/Isabelle2021...v1.3.0/Isabelle2021-1
+[v1.2.0]: https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF/compare/v1.1.0/Isabelle2021...v1.2.0/Isabelle2021
+[v1.1.0]: https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF/compare/v1.0.0/Isabelle2019...v1.1.0/Isabelle2021

CITATION

@@ -1,5 +1,4 @@
 To cite Isabelle/DOF in publications, please use
-
   
   Achim D. Brucker, Idir Ait-Sadoune, Paolo Crisafulli, and Burkhart
   Wolff. Using The Isabelle Ontology Framework: Linking the Formal

README.md

@@ -2,54 +2,51 @@
 
 Isabelle/DOF is a novel Document Ontology Framework on top of Isabelle.
 Isabelle/DOF allows for both conventional typesetting as well as formal
-development. The manual for [Isabelle/DOF 1.2.0/Isabelle2021 is available 
+development. The manual for [Isabelle/DOF 1.2.0/Isabelle2021 is available
 online.](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.2.0_Isabelle2021.pdf)
 
-## Running Isabelle/DOF using Docker
-
-As an alternative to installing Isabelle/DOF locally, the latest official release Isabelle/DOF
-is also available on Docker Hub. Thus, if you have Docker installed and your installation of
-Docker supports X11 application, you can start Isabelle/DOF as follows:
-
-```console
-foo@bar:~$ docker run -ti --rm -e DISPLAY=$DISPLAY -v /tmp/.X11-unix:/tmp/.X11-unix \ 
-           logicalhacking/isabelle_dof-1.2.0_isabelle2021 isabelle jedit
-```
-
 ## Pre-requisites
 
-Isabelle/DOF has two major pre-requisites:
+Isabelle/DOF has three major prerequisites:
 
-* **Isabelle:** Isabelle/DOF requires [Isabelle 2021](http://isabelle.in.tum.de/website-Isabelle2021/).
-  Please download the Isabelle 2021 distribution for your operating
-  system from the [Isabelle website](http://isabelle.in.tum.de/website-Isabelle2021/).
-* **LaTeX:** Isabelle/DOF requires a modern LaTeX installation, i.e., at least 
-  [TeX Live 2021](https://www.tug.org/texlive/) with all available updates applied.
+* **Isabelle:** Isabelle/DOF requires [Isabelle 2021-1](http://isabelle.in.tum.de/website-Isabelle2021-1/).
+  Please download the Isabelle 2021-1 distribution for your operating
+  system from the [Isabelle
+  website](http://isabelle.in.tum.de/website-Isabelle2021-1/).
+* **AFP:** Isabelle/DOF requires two entries from the [Archive of
+  Formal Proofs (AFP)](https://www.isa-afp.org/). Please install the
+  AFP following the instructions given at
+  <https://www.isa-afp.org/using.html>. For your convenience, we also
+  provide a script that only installs the two entries required by
+  Isabelle/DOF into the local Isabelle/DOF directory. First, Isabelle/DOF
+  needs to be registered as an Isabelle component:
+  
+  ```console
+  foo@bar:~$ isabelle components -u `pwd`
+  ```  
+
+  Thereafter, the AFP entries can be installed as follows:
+  
+  ```console
+  foo@bar:~$ isabelle env ./install-afp
+  ```  
+
+* **LaTeX:** Isabelle/DOF requires a modern LaTeX installation, i.e., at least
+  [TeX Live 2022](https://www.tug.org/texlive/) with all available updates applied.
   
 ## Installation
 
-In most case, the DOF-plugin can be installed as follows:
+Isabelle/DOF is provided as an Isabelle component. After installing the
+prerequisites, change into the directory containing Isabelle/DOF (this should be
+the directory containing this `README.md` file) and execute (if you executed
+this command already during the installation of the pre-requisites, you 
+can skip it now):
 
 ```console
-foo@bar:~$ ./install
+foo@bar:~$ isabelle components -u `pwd`
 ```
 
-If a specific Isabelle version should be used (i.e., not the default
-one), the full path to the ``isabelle`` command needs to be passed as
-using the ``--isabelle`` command line argument of the ``install`` script:
-
-```console
-foo@bar:~$ ./install --isabelle /usr/local/Isabelle2021/bin/isabelle
-```
-
-For further command line options of the installer, please use the
-built-in help:
-
-```console
-foo@bar:~$ ./install --help
-```
-
-A final step for the installation is:
+The final step for the installation is:
 
 ```console
 foo@bar:~$ isabelle build -D .
@@ -87,19 +84,19 @@ The DOF-plugin provides an alternative to Isabelle's ``mkroot`` command.
 Isabelle projects that use DOF need to be created using
 
 ```console
-foo@bar:~$ isabelle mkroot_DOF
+foo@bar:~$ isabelle dof_mkroot
 ```
 
-The ``mkroot_DOF`` command takes the same parameter as the standard
+The ``dof_mkroot`` command takes the same parameter as the standard
 ``mkroot`` command of Isabelle. Thereafter, the normal Isabelle
 command for building documents can be used.
 
 Using the ``-o`` option, different ontology setups can be
-selected and using the ``-t`` option, different LaTeX setups 
+selected and using the ``-t`` option, different LaTeX setups
 can be selected. For example,
 
 ```console
-foo@bar:~$ isabelle mkroot_DOF -o scholarly_paper -t scrartcl
+foo@bar:~$ isabelle dof_mkroot -o scholarly_paper -t scrartcl
 ```
 
 creates a setup using the scholarly_paper ontology and the article
@@ -109,33 +106,30 @@ The help (option ``-h``) show a list of all supported ontologies and
 document templates:
 
 ```console
-foo@bar:~$ isabelle mkroot_DOF -h
-
-Usage: isabelle mkroot_DOF [OPTIONS] [DIR]
+foo@bar:~$ isabelle dof_mkroot -h
+Usage: isabelle dof_mkroot [OPTIONS] [DIRECTORY]
 
   Options are:
-    -h           print this help text and exit
-    -n NAME      alternative session name (default: DIR base name)
-    -o ONTOLOGY  (default: scholarly_paper)
-       Available ontologies:
-       * cenelec_50128
-       * mathex
-       * scholarly_paper
-    -t TEMPLATE   (default: scrartcl)
-       Available document templates:
-       * lncs
-       * scrartcl
-       * scrreprt
-       * scrreprt-modern
+    -I           init Mercurial repository and add generated files
+    -n NAME      alternative session name (default: directory base name)
+    -o ONTOLOGY  ontology (default: scholarly_paper)
+    -t TEMPLATE  tempalte (default: scrartcl)
 
-  Prepare session root DIR (default: current directory).
+  Prepare session root directory (default: current directory).
 ```
 
 ## Releases
 
-For releases, signed archives including a PDF version of the Isabelle/DOF manual are
+For releases, signed archives including a PDF version of the Isabelle/DOF manual
 are available:
 
+* Isabelle/DOF 1.3.0/Isabelle2021-1
+  * [Isabelle_DOF-1.3.0_Isabelle2021-1.pdf](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.3.0_Isabelle2021-1.pdf)
+  * [Isabelle_DOF-1.3.0_Isabelle2021-1.tar.xz](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.3.0_Isabelle2021-1.tar.xz)
+  * [Isabelle_DOF-1.3.0_Isabelle2021-1.tar.xz.asc](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.3.0_Isabelle2021-1.tar.xz.asc)
+
+### Older Releases 
+
 * Isabelle/DOF 1.2.0/Isabelle2021
   * [Isabelle_DOF-1.2.0_Isabelle2021.pdf](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.2.0_Isabelle2021.pdf)
   * [Isabelle_DOF-1.2.0_Isabelle2021.tar.xz](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.2.0_Isabelle2021.tar.xz)
@@ -165,7 +159,7 @@ Main contacts:
 * Idir Ait-Sadoune
 * Paolo Crisafulli
 * Chantal Keller
-* Nicolas Méric 
+* Nicolas Méric
 
 ## License
 
@@ -188,11 +182,11 @@ SPDX-License-Identifier: BSD-2-Clause
   Computer Science (11724), Springer-Verlag, 2019.
   [doi:10.1007/978-3-030-30446-1_15](https://doi.org/10.1007/978-3-030-30446-1_15).
 
-* Achim D. Brucker, Burkhart Wolff. [Using Ontologies in Formal Developments Targeting Certification](https://www.brucker.ch/bibliography/download/2019/brucker.ea-ontologies-certification-2019.pdf). In 
+* Achim D. Brucker, Burkhart Wolff. [Using Ontologies in Formal Developments Targeting Certification](https://www.brucker.ch/bibliography/download/2019/brucker.ea-ontologies-certification-2019.pdf). In
   Integrated Formal Methods (IFM). Lecture Notes in Computer Science (11918). Springer-Verlag 2019.
   [doi:10.1007/978-3-030-34968-4_4](http://dx.doi.org/10.1007/978-3-030-34968-4_4)  
 
-* Sergio Bezzecchi, Paolo Crisafulli, Charlotte Pichot, and Burkhart Wolff. [Making Agile Development 
+* Sergio Bezzecchi, Paolo Crisafulli, Charlotte Pichot, and Burkhart Wolff. [Making Agile Development
   Processes fit for V-style Certification Procedures.](https://hal.archives-ouvertes.fr/hal-01702815/document)
    In ERTS 2018. <https://hal.archives-ouvertes.fr/hal-01702815>
 

etc/build.props

@@ -0,0 +1,12 @@
+title = Isabelle/DOF
+module = $ISABELLE_HOME_USER/DOF/isabelle_dof.jar
+no_build = false
+requirements = \
+  env:ISABELLE_SCALA_JAR
+sources = \
+  src/scala/dof_document_build.scala \
+  src/scala/dof_mkroot.scala \
+  src/scala/dof_tools.scala
+services = \
+  isabelle_dof.DOF_Tools \
+  isabelle_dof.DOF_Document_Build$Engine

etc/options

@@ -0,0 +1,30 @@
+(* :mode=isabelle-options: *)
+
+section "Isabelle/DOF"
+
+public option dof_template : string = "scrreprt-modern"
+  -- "Default document template for Isabelle/DOF documents"
+
+public option dof_ontologies : string = "Isabelle_DOF.technical_report Isabelle_DOF.scholarly_paper"
+  -- "Isabelle/DOF ontologies (separated by blanks)"
+
+option dof_version : string = "1.3.0" 
+  -- "Isabelle/DOF version" 
+     (* "Unreleased" for development, semantic version for releases *)
+
+option dof_isabelle : string = "2021-1" 
+option dof_afp : string = "afp-2021-12-28"
+
+option dof_latest_version : string = "1.3.0"    
+option dof_latest_isabelle : string = "Isabelle2021-1"
+option dof_latest_doi : string = "10.5281/zenodo.6810799"
+option dof_generic_doi : string = "10.5281/zenodo.3370482"
+
+option dof_url : string = "https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF"
+  -- "Isabelle/DOF source repository"
+
+option dof_artifact_dir : string = "releases/Isabelle_DOF/Isabelle_DOF"
+  -- "Isabelle/DOF release artifacts"
+
+option dof_artifact_host : string = "artifacts.logicalhacking.com"
+

etc/settings

@@ -0,0 +1,5 @@
+# -*- shell-script -*- :mode=shellscript:
+
+ISABELLE_DOF_HOME="$COMPONENT"
+ISABELLE_DOCS="$ISABELLE_DOF_HOME/doc":"$ISABELLE_DOCS"
+

examples/CENELEC_50128/mini_odo/ROOT

@@ -1,11 +1,10 @@
 session "mini_odo" = "Isabelle_DOF" +
-  options [document = pdf, document_output = "output"]
+  options [document = pdf, document_output = "output", document_build = dof,
+           dof_ontologies = "Isabelle_DOF.technical_report Isabelle_DOF.cenelec_50128", dof_template = "Isabelle_DOF.scrreprt-modern"]
   theories
     "mini_odo"
   document_files
-    "isadof.cfg"
     "preamble.tex"
-    "build"
     "root.bib"
     "root.mst"
     "lstisadof.sty"
@@ -13,3 +12,4 @@ session "mini_odo" = "Isabelle_DOF" +
     "figures/odometer.jpeg"
     "figures/three-phase-odo.pdf"
     "figures/wheel-df.png"
+

examples/CENELEC_50128/mini_odo/document/build

@@ -1,46 +0,0 @@
-#!/usr/bin/env bash
-# Copyright (c) 2018-2019 The University of Sheffield. All rights reserved.
-#               2018 The University of Paris-Saclay. All rights reserved.
-#
-# 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
-    echo ""
-    echo "Error: Isabelle/DOF not installed"
-    echo "====="
-    echo "This is a Isabelle/DOF project. The document preparation requires"
-    echo "the Isabelle/DOF framework. Please obtain the framework by cloning"
-    echo "the Isabelle/DOF git repository, i.e.: "
-    echo "    git clone https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF"
-    echo "You can install the framework as follows:"
-    echo "    cd Isabelle_DOF/document-generator"
-    echo "    ./install"
-    echo ""
-    exit 1
-fi
-
-cp $ISABELLE_HOME_USER/DOF/document-template/build_lib.sh .
-source build_lib.sh

examples/CENELEC_50128/mini_odo/document/isadof.cfg

@@ -1,3 +0,0 @@
-Template: scrreprt-modern
-Ontology: technical_report
-Ontology: cenelec_50128

examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy

@@ -256,7 +256,7 @@ enforcing a sequence of text-elements that must belong to the corresponding clas
 To start using \<^isadof>, one creates an Isabelle project (with the name 
 \inlinebash{IsaDofApplications}):
 \begin{bash}
-  isabelle mkroot_DOF -o scholarly_paper -t lncs -d  IsaDofApplications
+  isabelle dof_mkroot -o scholarly_paper -t lncs IsaDofApplications
 \end{bash}
 where the \inlinebash{-o scholarly_paper} specifies the ontology for writing scientific articles and 
 \inlinebash{-t lncs} specifies the use of Springer's \LaTeX-configuration for the Lecture Notes in 

examples/scholarly_paper/2018-cicm-isabelle_dof-applications/ROOT

@@ -1,13 +1,15 @@
 session "2018-cicm-isabelle_dof-applications" = "Isabelle_DOF" + 
-  options  [document = pdf, document_output = "output", quick_and_dirty = true]
+  options  [document = pdf, document_output = "output", document_build = dof,
+   dof_ontologies = "Isabelle_DOF.scholarly_paper", dof_template = Isabelle_DOF.lncs, 
+   quick_and_dirty = true]
   theories
     IsaDofApplications
   document_files
-    "isadof.cfg"
     "root.bib"
+    "authorarchive.sty"
     "preamble.tex"
-    "build"
     "lstisadof.sty"
+    "vector_iD_icon.pdf"
     "figures/isabelle-architecture.pdf"
     "figures/Dogfood-Intro.png"
     "figures/InteractiveMathSheet.png"

examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/authorarchive.sty

@@ -0,0 +1,339 @@
+%% Copyright (C) 2008-2019 Achim D. Brucker, https://www.brucker.ch
+%%
+%% License:
+%%   This program can be redistributed and/or modified under the terms
+%%   of the LaTeX Project Public License Distributed from CTAN
+%%   archives in directory macros/latex/base/lppl.txt; either
+%%   version 1.3c of the License, or (at your option) any later version.
+%%   OR
+%%   The 2-clause BSD-style license.
+%%
+%%   SPDX-License-Identifier: LPPL-1.3c+ OR BSD-2-Clause
+\NeedsTeXFormat{LaTeX2e}\relax
+\ProvidesPackage{authorarchive}
+  [0000/00/00 Unreleased v1.1.1+%
+  Self-archiving information for scientific publications.]
+%
+\PassOptionsToPackage{hyphens}{url}
+%
+\RequirePackage{ifthen}
+\RequirePackage[inline]{enumitem}
+\RequirePackage{graphicx}
+\RequirePackage{eso-pic}
+\RequirePackage{intopdf}
+\RequirePackage{kvoptions}
+\RequirePackage{hyperref}
+\RequirePackage{calc}
+\RequirePackage{qrcode}
+\RequirePackage{hvlogos}
+%
+%Better url breaking
+\g@addto@macro{\UrlBreaks}{\UrlOrds}
+%
+% Option declarations
+% -------------------
+\SetupKeyvalOptions{
+  family=AA,
+  prefix=AA@
+}
+%
+\DeclareStringOption[.]{bibtexdir}
+\DeclareStringOption[https://duckduckgo.com/?q=]{baseurl}
+\DeclareStringOption[.pdf]{suffix}
+\DeclareStringOption[UNKNOWN PUBLISHER]{publisher}[]
+\DeclareStringOption[UNKNOWN YEAR]{year}[]
+\DeclareStringOption[]{key}[]
+\DeclareStringOption[]{doi}[]
+\DeclareStringOption[]{doiText}[]
+\DeclareStringOption[]{publisherurl}[]
+\DeclareStringOption[UNKNOWN START PAGE]{startpage}[]
+\DeclareStringOption[UNKNOWN PUBLICATION]{publication}[]
+
+\DeclareBoolOption{ACM}
+\DeclareBoolOption{acmart}
+\DeclareBoolOption{ENTCS}
+\DeclareBoolOption{IEEE}
+\DeclareBoolOption{LNCS}
+\DeclareBoolOption{LNI}
+\DeclareBoolOption{nocopyright}
+\DeclareBoolOption{nourl}
+\DeclareBoolOption{nobib}
+\DeclareBoolOption{orcidicon}
+%\ProcessOptions\relax
+
+
+% Default option rule
+\DeclareDefaultOption{%
+  \ifx\CurrentOptionValue\relax
+    \PackageWarningNoLine{\@currname}{%
+      Unknown option `\CurrentOption'\MessageBreak
+      is passed to package `authorarchive'%
+    }%
+    % Pass the option to package color.
+    % Again it is better to expand \CurrentOption.
+    \expandafter\PassOptionsToPackage\expandafter{\CurrentOption}{color}%
+  \else
+    % Package color does not take options with values.
+    % We provide the standard LaTeX error.
+    \@unknownoptionerror
+  \fi
+}
+\ProcessKeyvalOptions*
+
+% Provide command for dynamic configuration seutp
+\def\authorsetup{\kvsetkeys{AA}}
+
+% Load local configuration
+\InputIfFileExists{authorarchive.config}{}{}
+
+
+\newlength\AA@x
+\newlength\AA@y
+\newlength\AA@width
+
+\def\AA@bibBibTeX{\AA@bibtexdir/\AA@key.bib}
+\def\AA@bibBibTeXLong{\AA@bibtexdir/\AA@key.bibtex}
+\def\AA@bibWord{\AA@bibtexdir/\AA@key.word.xml}
+\def\AA@bibEndnote{\AA@bibtexdir/\AA@key.enw}
+\def\AA@bibRIS{\AA@bibtexdir/\AA@key.ris}
+
+\newboolean{AA@bibExists}
+\setboolean{AA@bibExists}{false}
+\IfFileExists{\AA@bibBibTeX}{\setboolean{AA@bibExists}{true}}{}
+\IfFileExists{\AA@bibBibTeXLong}{\setboolean{AA@bibExists}{true}}{}
+\IfFileExists{\AA@bibWord}{\setboolean{AA@bibExists}{true}}{}
+\IfFileExists{\AA@bibEndnote}{\setboolean{AA@bibExists}{true}}{}
+\IfFileExists{\AA@bibRIS}{\setboolean{AA@bibExists}{true}}{}
+
+\setlength\AA@x{1in+\hoffset+\oddsidemargin}
+
+\newcommand{\authorcrfont}{\footnotesize}
+\newcommand{\authorat}[1]{\AtPageUpperLeft{\put(\LenToUnit{\AA@x},\LenToUnit{.2cm-\paperheight}){#1}}}
+\newcommand{\authorwidth}[1]{\setlength{\AA@width}{#1}}
+\setlength{\AA@width}{\textwidth}
+
+\def\AA@pageinfo{}
+\ifthenelse{\equal{\AA@startpage}{UNKNOWN START PAGE}}{%
+}{%
+  \setcounter{page}{\AA@startpage}%
+  \def\AA@pageinfo{pp. \thepage--\pageref{\aa@lastpage}, }
+}
+
+
+
+%%%% sig-alternate.cls
+\ifAA@ACM%
+  \ifthenelse{\equal{\AA@publisher}{UNKNOWN PUBLISHER}}{%
+    \setkeys{AA}{publisher=ACM}
+  }{}
+  \global\boilerplate={}
+  \global\copyrightetc={}
+  \renewcommand{\conferenceinfo}[2]{}
+  \renewcommand{\authorcrfont}{\scriptsize}
+  \setlength\AA@x{1in+\hoffset+\oddsidemargin}
+  \setlength\AA@y{-\textheight+\topmargin+\headheight-\footskip} % -\voffset-\topmargin-\headheight-\footskip}
+  \renewcommand{\authorat}[1]{\put(\LenToUnit{\AA@x},\LenToUnit{\AA@y}){#1}}
+  \setlength{\AA@width}{\columnwidth}
+\fi
+%
+%%%% acmart.cls
+\ifAA@acmart%
+  \ifthenelse{\equal{\AA@publisher}{UNKNOWN PUBLISHER}}{%
+    \setkeys{AA}{publisher=ACM}
+  }{}
+  \renewcommand{\authorat}[1]{\AtPageUpperLeft{\put(\LenToUnit{\AA@x},\LenToUnit{0.2cm-\paperheight}){#1}}}
+  \setlength{\AA@width}{\textwidth}
+\fi
+%
+%%%% LNCS
+\ifAA@LNCS%
+  \ifAA@orcidicon%
+    \renewcommand{\orcidID}[1]{\href{https://orcid.org/#1}{%
+      \textsuperscript{\,\includegraphics[height=2\fontcharht\font`A]{vector_iD_icon}}}}
+  \else\relax\fi%
+%  
+  \ifthenelse{\equal{\AA@publisher}{UNKNOWN PUBLISHER}}{%
+    \setkeys{AA}{publisher=Springer-Verlag}
+  }{}
+  \renewcommand{\authorcrfont}{\scriptsize}
+  \@ifclasswith{llncs}{a4paper}{%
+    \ExplSyntaxOn
+    \@ifundefined{pdfmanagement_add:nnn}{%
+      \pdfpagesattr{/CropBox [92 114 523 780]}%
+    }{%
+      \pdfmanagement_add:nnn {Pages}{CropBox}{[92~114~523~780]}
+    }%
+    \ExplSyntaxOff
+    \renewcommand{\authorat}[1]{\put(\LenToUnit{\AA@x},40){#1}}%
+  }{%
+    \ExplSyntaxOn
+    \@ifundefined{pdfmanagement_add:nnn}{%
+      \pdfpagesattr{/CropBox [92 65 523 731]}% LNCS page: 152x235 mm
+    }{%
+      \pdfmanagement_add:nnn {Pages}{CropBox}{[92~62~523~731]}
+    }%
+    \ExplSyntaxOff
+    \renewcommand{\authorat}[1]{\put(\LenToUnit{\AA@x},23){#1}}
+  }
+  \setlength{\AA@width}{\textwidth}
+  \setcounter{tocdepth}{2}
+\fi
+%
+%%%% LNI
+\ifAA@LNI%
+  \ifthenelse{\equal{\AA@publisher}{UNKNOWN PUBLISHER}}{%
+    \setkeys{AA}{publisher=GI}
+  }{}
+  \renewcommand{\authorat}[1]{\put(\LenToUnit{\AA@x},35){#1}}
+  \renewcommand{\authorcrfont}{\scriptsize}
+  \pdfpagesattr{/CropBox [70 65 526.378 748.15]} % TODO
+  \setlength{\AA@width}{\textwidth}
+  \setcounter{tocdepth}{2}
+\fi
+%
+%%%% ENTCS
+\ifAA@ENTCS%
+  \addtolength{\voffset}{1cm}
+  \ifthenelse{\equal{\AA@publisher}{UNKNOWN PUBLISHER}}{%
+    \setkeys{AA}{publisher=Elsevier Science B.~V.}
+  }{}
+  \renewcommand{\authorat}[1]{\put(\LenToUnit{\AA@x},\LenToUnit{-.5cm-\the\ht\AA@authoratBox}){#1}}
+  \renewcommand{\authorcrfont}{\scriptsize}
+  \setlength{\AA@width}{\textwidth}
+\fi
+%
+%%%% IEEE
+\ifAA@IEEE%
+  \ifthenelse{\equal{\AA@publisher}{UNKNOWN PUBLISHER}}{%
+    \setkeys{AA}{publisher=IEEE}
+  }{}
+  \renewcommand{\authorat}[1]{\put(\LenToUnit{\AA@x},6){#1}}
+  \renewcommand{\authorcrfont}{\scriptsize}
+  \setlength{\AA@width}{\textwidth}
+  \setcounter{tocdepth}{2}
+\fi
+%
+
+\hypersetup{%
+  draft         = false,
+  bookmarksopen = true,
+  bookmarksnumbered= true,
+  pdfauthor     = {\@author},
+  pdftitle      = {\@title},
+}
+
+\@ifpackageloaded{totpages}{%
+  \def\aa@lastpage{TotPages}
+}{%
+  \RequirePackage{lastpage}
+  \def\aa@lastpage{LastPage}
+}
+\newsavebox{\AA@authoratBox}
+
+\AddToShipoutPicture*{%
+  \setlength{\unitlength}{1mm}%
+  \savebox{\AA@authoratBox}{%
+    \parbox{1.4cm}{%
+      \bgroup%
+        \normallineskiplimit=0pt%
+        \ifAA@nourl%
+           \ifx\AA@doi\@empty\relax%
+           \else%
+              \qrcode[hyperlink,height=1.17cm,padding]{https://doi.org/\AA@doi}%
+            \fi%
+        \else%
+          \qrcode[hyperlink,height=1.17cm,padding]{\AA@baseurl/\AA@key\AA@suffix}%
+        \fi%
+      \egroup%
+    }%
+    \ifAA@nourl\ifx\AA@doi\@empty\addtolength{\AA@width}{1.4cm}\fi\fi
+    \parbox{\AA@width-1.4cm}{\authorcrfont%
+      \ifAA@LNCS%
+        \AA@publication, \AA@pageinfo  \AA@year. %
+        \ifAA@nocopyright\else
+          \textcopyright~\AA@year~\AA@publisher.
+        \fi
+        This is the author's
+        version of the work. It is posted
+        \ifAA@nourl\relax\else%
+          at \url{\AA@baseurl/\AA@key\AA@suffix} %
+        \fi
+        \ifAA@nocopyright\relax\else
+          by permission of \AA@publisher{}
+        \fi
+        for your personal use.
+        \ifx\AA@doi\@empty%
+          \relax
+        \else
+          The final publication is available at Springer via
+          \ifx\AA@doiText\@empty%
+            \url{https://doi.org/\AA@doi}.
+          \else
+            \href{https://doi.org/\AA@doi}{\AA@doiText}.
+          \fi
+        \fi
+      \else
+        \ifAA@nocopyright\relax\else
+          \textcopyright~\AA@year~\AA@publisher. %
+        \fi%
+        This is the author's
+        version of the work. It is posted
+        \ifAA@nourl\relax\else%
+          at \url{\AA@baseurl/\AA@key\AA@suffix} %
+        \fi
+        \ifAA@nocopyright\relax\else
+          by permission of \AA@publisher{} %
+        \fi
+        for your personal use. Not for redistribution. The definitive
+        version was published in \emph{\AA@publication}, \AA@pageinfo \AA@year%
+        \ifx\AA@doi\@empty%
+          \ifx\AA@publisherurl\@empty%
+            .%
+          \else
+            \url{\AA@publisherurl}.%
+          \fi
+        \else
+          \ifx\AA@doiText\@empty%
+            , doi: \href{https://doi.org/\AA@doi}{\AA@doi}.%
+          \else
+            , doi: \href{https://doi.org/\AA@doi}{\AA@doiText}.%
+          \fi
+        \fi
+      \fi
+      \ifAA@nobib\relax\else%
+        \ifthenelse{\boolean{AA@bibExists}}{%
+          \hfill
+          \begin{itemize*}[label={}, itemjoin={,}]
+            \IfFileExists{\AA@bibBibTeX}{%
+              \item \attachandlink{\AA@bibBibTeX}[application/x-bibtex]{BibTeX entry of this paper}{\BibTeX}%
+            }{%
+              \IfFileExists{\AA@bibBibTeXLong}{%
+                \item \attachandlink[\AA@key.bib]{\AA@bibBibTeXLong}[application/x-bibtex]{BibTeX entry of this paper}{\BibTeX}%
+              }{%
+                \typeout{No file \AA@bibBibTeX{} (and no \AA@bibBibTeXLong) found. Not embedded reference in BibTeX format.}%
+              }%
+            }%
+            \IfFileExists{\AA@bibWord}{%
+              \item \attachandlink{\AA@bibWord}[application/xml]{XML entry of this paper (e.g., for Word 2007 and later)}{Word}%
+            }{%
+              \typeout{No file \AA@bibWord{} found. Not embedded reference for Word 2007 and later.}%
+            }%
+            \IfFileExists{\AA@bibEndnote}{%
+              \item \attachandlink{\AA@bibEndnote}[application/x-endnote-refer]{Endnote entry of this paper}{EndNote}%
+            }{%
+              \typeout{No file \AA@bibEndnote{} found. Not embedded reference in Endnote format.}%
+            }%
+            \IfFileExists{\AA@bibRIS}{%
+              \item \attachandlink{\AA@bibRIS}[application/x-research-info-systems]{RIS entry of this paper}{RIS}%
+            }{%
+              \typeout{No file \AA@bibRIS{} found. Not embedded reference in RIS format.}%
+            }%
+          \end{itemize*}\\
+        }{%
+          \PackageError{authorarchive}{No bibliographic files found. Specify option 'nobib' if this is intended.}
+        }
+      \fi
+    }
+  }
+  \authorat{\raisebox{\the\ht\AA@authoratBox}{\usebox{\AA@authoratBox}}}
+}

examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/build

@@ -1,46 +0,0 @@
-#!/usr/bin/env bash
-# Copyright (c) 2018-2019 The University of Sheffield. All rights reserved.
-#               2018 The University of Paris-Saclay. All rights reserved.
-#
-# 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
-    echo ""
-    echo "Error: Isabelle/DOF not installed"
-    echo "====="
-    echo "This is a Isabelle/DOF project. The document preparation requires"
-    echo "the Isabelle/DOF framework. Please obtain the framework by cloning"
-    echo "the Isabelle/DOF git repository, i.e.: "
-    echo "    git clone https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF"
-    echo "You can install the framework as follows:"
-    echo "    cd Isabelle_DOF/document-generator"
-    echo "    ./install"
-    echo ""
-    exit 1
-fi
-
-cp $ISABELLE_HOME_USER/DOF/document-template/build_lib.sh .
-source build_lib.sh

examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/isadof.cfg

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

examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/preamble.tex

@@ -53,23 +53,18 @@
 \usepackage[size=footnotesize]{caption}
 
 
-\subject{Example of an Academic Paper\footnote{%
-  This document is an example setup for writing an academic paper. While
-  it is optimized for the Springer's LNCS class, it uses a Koma Script
-  LaTeX class to avoid the re-distribution of \texttt{llncs.cls},
-  which would violate Springer's copyright. This example has been
-  published at CICM 2018:
-    \protect\begin{quote}
-      Achim D. Brucker, Idir Ait-Sadoune, Paolo Crisafulli, and
-      Burkhart Wolff. Using The Isabelle Ontology Framework: Linking
-      the Formal with the Informal. In Conference on Intelligent
-      Computer Mathematics (CICM). Lecture Notes in Computer Science
-      (11006), Springer-Verlag, 2018. 
-    \protect\end{quote}
-    Note that the content of this example is not updated and, hence,
-    might not be correct with respect to the latest version of
-    \isadof{}. 
-    }}
+\usepackage[LNCS,
+   orcidicon,
+   key=brucker.ea-isabelle-ontologies-2018,
+   year=2018,
+   publication={F. Rabe et al. (Eds.): CICM 2018, LNAI 11006},
+   nobib,
+   startpage={1},
+   doi={10.1007/978-3-319-96812-4_3},
+   doiText={10.1007/978-3-319-96812-4\_3},
+]{authorarchive}
+\authorrunning{A. D. Brucker et al.}
+\pagestyle{headings}
 
 
 \title{<TITLE>}

examples/scholarly_paper/2020-iFM-CSP/ROOT

@@ -1,9 +1,8 @@
 session "2020-iFM-csp" = "Isabelle_DOF" +
-  options [document = pdf, document_output = "output"]
+  options [document = pdf, document_output = "output", document_build = dof,
+  dof_ontologies = "Isabelle_DOF.scholarly_paper", dof_template = Isabelle_DOF.scrartcl]
   theories
     "paper"
   document_files
-    "isadof.cfg"
     "root.bib"
     "preamble.tex"
-    "build"

examples/scholarly_paper/2020-iFM-CSP/document/build

@@ -1,47 +0,0 @@
-#!/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/2020-iFM-CSP/document/isadof.cfg

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

examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy

@@ -29,20 +29,6 @@ text\<open>
 \<close>
 
 section*[getting_started::technical]\<open>Getting Started\<close>
-text\<open>
-As an alternative to installing \<^isadof>{} locally, the latest official release of \<^isadof> is also 
-available on \href{https://cloud.docker.com/u/logicalhacking/}{Docker Hub}. Thus, if you have 
-\href{https://www.docker.com}{Docker} installed and 
-your installation of Docker supports X11 application, you can start \<^isadof> as follows:
-
-@{boxed_bash [display] \<open>ë\prompt{}ë docker run -ti --rm -e DISPLAY=$DISPLAY \
-   -v /tmp/.X11-unix:/tmp/.X11-unix \ 
-   logicalhacking/isabelle_dof-ë\doflatestversionë_ë\MakeLowercase{\isabellelatestversion}ë \
-   isabelle jedit\<close>}
-
-Further configuration of the X11 permissions to authorize docker to start \<^isadof> might be required,
-depending on the user system configuration.
-\<close>
 
 subsection*[installation::technical]\<open>Installation\<close>
 text\<open>
@@ -50,8 +36,8 @@ text\<open>
   \<^LaTeX>. We assume a basic familiarity with a Linux/Unix-like command line (i.e., a shell). 
 
   \<^isadof> requires Isabelle\<^bindex>\<open>Isabelle\<close> (\isabellefullversion) with a recent \<^LaTeX>-distribution
-  (e.g., Tex Live 2021 or later).    
-  \<^isadof> uses a two-part version system (e.g., 1.1.0/Isabelle2021),  where the first part is the version
+  (e.g., Tex Live 2022 or later).    
+  \<^isadof> uses a two-part version system (e.g., 1.2.0/Isabelle2021),  where the first part is the version
   of \<^isadof> (using semantic versioning) and the second part is the supported version of Isabelle. 
   Thus, the same version of \<^isadof> might be available for different versions of Isabelle. 
 \<close>
@@ -68,7 +54,7 @@ text\<open>
 Depending on your operating system and depending if you put Isabelle's  \<^boxed_bash>\<open>bin\<close> directory
 in your  \<^boxed_bash>\<open>PATH\<close>, you will need to invoke  \<^boxed_bash>\<open>isabelle\<close> using its
 full qualified path, \<^eg>:
-@{boxed_bash [display]\<open>ë\prompt{}ë /usr/local/Isabelleë\isabelleversionë/bin/isabelle version
+@{boxed_bash [display]\<open>ë\prompt{}ë /usr/local/Isabelleë\isabelleversion/bin/isabelleë version
 ë\isabellefullversionë\<close>}
 \<close>
 
@@ -83,36 +69,30 @@ text\<open>
 subsubsection*[isadof::technical]\<open>Installing \<^isadof>\<close>
 text\<open>
   In the following, we assume that you already downloaded the \<^isadof> distribution 
-  (\href{\isadofarchiveurl}{\isadofarchiven}) from the \<^isadof> web site. The main steps for 
-  installing are extracting the \<^isadof> distribution and calling its \<^boxed_bash>\<open>install\<close> script. 
+  (\href{\isadofarchiveurl}{\isadofarchiven}) from the \<^isadof> web site. 
   We start by extracting the \<^isadof> archive:
 @{boxed_bash [display]\<open>ë\prompt{}ë tar xf ë\href{\isadofarchiveurl}{\isadofarchiven}ë\<close>}
 This will create a directory \texttt{\isadofdirn} containing \<^isadof> distribution.
-Next, we need to invoke the \<^boxed_bash>\<open>install\<close> script. If necessary, the installation 
-automatically downloads additional dependencies from the AFP (\<^url>\<open>https://www.isa-afp.org\<close>), 
-namely the AFP  entries ``Functional Automata''~@{cite "nipkow.ea:functional-Automata-afp:2004"} 
-and ``Regular Sets and Expressions''~@{cite "kraus.ea:regular-sets-afp:2010"}. This might take a 
-few minutes to complete. Moreover, the installation script applies a patch to the Isabelle system, 
-which requires  \<^emph>\<open>write permissions for the Isabelle system directory\<close> and registers \<^isadof> as 
-Isabelle component. 
 
-If the \<^boxed_bash>\<open>isabelle\<close> tool is not in your  \<^boxed_bash>\<open>PATH\<close>, you need to call the 
- \<^boxed_bash>\<open>install\<close> script with the  \<^boxed_bash>\<open>--isabelle\<close> option, passing the full-qualified
-path of the \<^boxed_bash>\<open>isabelle\<close> tool ( \<^boxed_bash>\<open>install --help\<close> gives 
-you an overview of all available configuration options):
+Next, we need to register \<^isadof> as an Isabelle component:
+
+@{boxed_bash [display]\<open>ë\prompt{}ë isabelle components -u ë\mbox{\isadofdirn}ë\<close>}
+
+Moreover, \<^isadof> depends on the the AFP (\<^url>\<open>https://www.isa-afp.org\<close>), namely the AFP  
+entries ``Functional Automata''~@{cite "nipkow.ea:functional-Automata-afp:2004"} and 
+``Regular Sets and Expressions''~@{cite "kraus.ea:regular-sets-afp:2010"}. You can either
+install the complete AFP, following the instructions given at \<^url>\<open>https://www.isa-afp.org/using.html\<close>), 
+or use the provided \<^boxed_bash>\<open>install\<close> script to install a minimal AFP 
+setup into the local \<^isadof> directory. The script needs to be prefixed with the 
+\<^boxed_bash>\<open>isabelle eëënv\<close> command:
 
 @{boxed_bash [display]\<open>ë\prompt{}ë cd ë\isadofdirnë
-ë\prompt{\isadofdirn}ë ./install --isabelle /usr/local/Isabelleë\isabelleversion/bin/isabelleë
+ë\prompt{\isadofdirn}ë isabelle eëënv ë\mbox{./install-afp}ë
 
 Isabelle/DOF Installer
 ======================
 * Checking Isabelle version:
   Success: found supported Isabelle version ë(\isabellefullversion)ë
-* Check availability of Isabelle/DOF patch:
-  Warning: Isabelle/DOF patch is not available or outdated.
-           Trying to patch system ....
-       Applied patch successfully, Isabelle/HOL will be rebuilt during
-       the next start of Isabelle.
 * Checking availability of AFP entries:\<close>}
 
 @{boxed_bash [display]
@@ -124,18 +104,6 @@ Isabelle/DOF Installer
            Registering Functional-Automata iëën 
                  /home/achim/.isabelle/Isabelleë\isabelleversion/ROOTSë
            AFP installation successful.
-* Searching fëëor existing installation:
-  No old installation found.
-* Installing Isabelle/DOF
-  - Installing Tools iëën 
-        /home/achim/.isabelle/Isabelleë\isabelleversion/DOF/Toolsë
-  - Installing document templates iëën 
-        /home/achim/.isabelle/Isabelleë\isabelleversion/DOF/document-templateë
-  - Installing LaTeX styles iëën 
-       /home/achim/.isabelle/Isabelleë\isabelleversion/DOF/latexë
-  - Registering Isabelle/DOF
-    * Registering tools iëën 
-       /home/achim/.isabelle/Isabelleë\isabelleversion/etc/settingsë
 * Installation successful. Enjoy Isabelle/DOF, you can build the session
   Isabelle/DOF and all example documents by executing:
   /usr/local/Isabelleë\isabelleversion/bin/isabelleë build -D . \<close>}
@@ -150,15 +118,17 @@ session and all example documents, execute:
 subsection*[first_project::technical]\<open>Creating an \<^isadof> Project\<close>
 text\<open>
   \<^isadof> provides its own variant of Isabelle's 
-  \<^boxed_bash>\<open>mkroot\<close> tool, called \<^boxed_bash>\<open>mkroot_DOF\<close>\index{mkroot\_DOF}:
-@{boxed_bash [display]\<open>ë\prompt{}ë isabelle mkroot_DOF myproject
+  \<^boxed_bash>\<open>mkroot\<close> tool, called \<^boxed_bash>\<open>dof_mkroot\<close>\index{mkroot\_DOF}:
+@{boxed_bash [display]\<open>ë\prompt{}ë isabelle dof_mkroot myproject
 
 Preparing session "myproject" iëën "myproject"
   creating "myproject/ROOT"
-  creating "myproject/document/root.tex"
+  creating "myproject/myproject.thy"
+  creating "myproject/document/preamble.tex"
 
-Now use the following coëëmmand line to build the session:
-  isabelle build -D myproject \<close>}
+Now use the following commanëëd line to build the session:
+
+  isabelle build -D myproject\<close>}
   The created project uses the default configuration (the ontology for writing academic papers 
   (scholarly\_paper) using a report layout based on the article class (\<^boxed_latex>\<open>scrartcl\<close>) of 
   the KOMA-Script bundle~@{cite "kohm:koma-script:2019"}). The directory \<^boxed_bash>\<open>myproject\<close> 
@@ -174,22 +144,26 @@ The directory  \<^boxed_bash>\<open>myproject\<close> contains the following fil
 .1 .
 .2 myproject.
 .3 document.
-.4 build\DTcomment{Build Script}.
-.4 isadof.cfg\DTcomment{\<^isadof> configuration}.
 .4 preamble.tex\DTcomment{Manual \<^LaTeX>-configuration}.
+.3 myproject.thy\DTcomment{Example theory file}.
 .3 ROOT\DTcomment{Isabelle build-configuration}.
 }
 \end{minipage}
 \end{center}
-The \<^isadof> configuration (\<^boxed_bash>\<open>isadof.cfg\<close>) specifies the required
-ontologies and the document template using a YAML syntax.\<^footnote>\<open>Isabelle power users will recognize that 
+
+The main two configuration files\<^footnote>\<open>Isabelle power users will recognize that
 \<^isadof>'s document setup does not make use of a file \<^boxed_bash>\<open>root.tex\<close>: this file is 
-replaced by built-in document templates.\<close> The main two configuration files for 
-users are:
+replaced by built-in document templates.\<close>  for users are: 
 \<^item> The file \<^boxed_bash>\<open>ROOT\<close>\<^index>\<open>ROOT\<close>, which defines the Isabelle session. New theory files as well as new 
   files required by the document generation (\<^eg>, images, bibliography database using \<^BibTeX>, local
   \<^LaTeX>-styles) need to be registered in this file. For details of Isabelle's build system, please 
-  consult the Isabelle System Manual~@{cite "wenzel:system-manual:2020"}.
+  consult the Isabelle System Manual~@{cite "wenzel:system-manual:2020"}. In addition to the 
+  standard features of, this file also contains \<^isadof> specific configurations:
+  \<^item>  \<^boxed_bash>\<open>dof_ontologies\<close> a list of (fully qualified) ontologies, separated by spaces, used 
+     by the project. 
+  \<^item>  \<^boxed_bash>\<open>dof_template\<close> the (fully qualified) document template.
+  \<^item>  \<^boxed_bash>\<open>document_build=dof\<close> needs to be present, to tell Isabelle, to use the 
+  Isabelle/DOF backend for the document generation.
 \<^item> The file \<^boxed_bash>\<open>preamble.tex\<close>\<^index>\<open>preamble.tex\<close>, which allows users to add additional 
   \<^LaTeX>-packages or to add/modify \<^LaTeX>-commands. 
 \<close>
@@ -202,32 +176,21 @@ text\<open>
     obtains and adds the necessary \<^LaTeX> class file. 
     This is due to licensing restrictions).\<close>
 text\<open> 
-  This can be configured by using the command-line options of \<^boxed_bash>\<open>mkroot_DOF\<close>. In 
+  This can be configured by using the command-line options of \<^boxed_bash>\<open>dof_mkroot\<close>. In 
   Particular, \<^boxed_bash>\<open>-o\<close> allows selecting the ontology and \<^boxed_bash>\<open>-t\<close> allows selecting 
-  the document template. The built-in help (using  \<^boxed_bash>\<open>-h\<close>) shows all available options 
-  as well as a complete list of the available document templates and ontologies: 
+  the document template. The built-in help (using  \<^boxed_bash>\<open>-h\<close>) shows all available options: 
 
-  @{boxed_bash [display]\<open>ë\prompt{}ë isabelle mkroot_DOF -h
+  @{boxed_bash [display]\<open>ë\prompt{}ë isabelle dof_mkroot -h
 
-Usage: isabelle mkroot_DOF [OPTIONS] [DIR]
+Usage: isabelle dof_mkroot [OPTIONS] [DIRECTORY]
 
   Options are:
-    -h           print this hëëelp text and exëëit
-    -n NAME      alternative session name (default: DIR base name)
-    -o ONTOLOGY  (default: scholarly_paper)
-       Available ontologies:
-       * CENELEC_50128
-       * math_exam
-       * scholarly_paper
-       * technical_report
-    -t TEMPLATE   (default: scrartcl)
-       Available document templates:
-       * lncs
-       * scrartcl
-       * scrreprt-modern
-       * scrreprt
+    -I           init Mercurial repository and add generated files
+    -n NAME      alternative session name (default: directory base name)
+    -o ONTOLOGY  ontology (default: scholarly_paper)
+    -t TEMPLATE  tempalte (default: scrartcl)
 
-  Prepare session root DIR (default: current directory). \<close>}
+  Prepare session root directory (default: current directory).\<close>}
 
 \<close>
 
@@ -541,9 +504,6 @@ side_by_side_figure*["hyperlinks"::side_by_side_figure,anchor="''fig:Dogfood-IV-
                       caption2="''Exploring an attribute (hyperlinked to the class).''",
                       relative_width2="47",
                       src2="''figures/Dogfood-V-attribute''"]\<open>Navigation via generated hyperlinks.\<close>
-(* TODO: Update the images in fig:Dogfood-IV-jumpInDocCLass side_by_side_figure
-   to align them. This has to wait that the exploration of an attribute is again possible.
-   See: https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF/issues/10 *)
 
 text\<open> 
   From these class definitions, \<^isadof> also automatically generated editing 

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

@@ -324,21 +324,28 @@ is currently only available in the SML API's of the kernel.
   as specified in @{technical \<open>odl-manual0\<close>}.
 \<^item> \<open>meta_args\<close> : 
    \<^rail>\<open>obj_id ('::' class_id) ((',' attribute '=' HOL_term) *) \<close>
+\<^item> \<^emph>\<open>evaluator\<close>: from @{cite "wenzel:isabelle-isar:2020"}, evaluation is tried first using ML,
+  falling back to normalization by evaluation if this fails. Alternatively a specific
+  evaluator can be selected using square brackets; typical evaluators use the
+  current set of code equations to normalize and include \<open>simp\<close> for fully
+  symbolic evaluation using the simplifier, \<open>nbe\<close> for \<^emph>\<open>normalization by
+  evaluation\<close> and \<^emph>\<open>code\<close> for code generation in SML.
 \<^item> \<open>upd_meta_args\<close> :
-   \<^rail>\<open> (obj_id ('::' class_id) ((',' attribute ('=' | '+=') HOL_term) * ))\<close>
+   \<^rail>\<open> (obj_id ('::' class_id) ((',' attribute (':=' | '+=') HOL_term) * ))\<close>
 \<^item> \<open>annotated_text_element\<close> :
 \<^rail>\<open> 
-    (  (  @@{command "text*"} '[' meta_args ']' '\<open>' formal_text '\<close>'
+    (  @@{command "text*"} '[' meta_args ']' '\<open>' formal_text '\<close>'
         | @@{command "ML*"}   ('[' meta_args ']')? '\<open>' SML_code '\<close>'
         | @@{command "term*"} ('[' meta_args ']')? '\<open>' HOL_term  '\<close>'
-        | @@{command "value*"} ('[' meta_args ']')? '\<open>' HOL_term  '\<close>'
-       )
-      |
-       (  @@{command "open_monitor*"}  
+        | @@{command "value*"} \<newline> ('[' meta_args ']' ('[' evaluator ']')?)? '\<open>' HOL_term  '\<close>'
+        | @@{command "assert*"} \<newline> ('[' meta_args ']' ('[' evaluator ']')?)? '\<open>' HOL_term '\<close>'
+    )
+  \<close>
+\<^rail>\<open>  
+     (  @@{command "open_monitor*"}  
         | @@{command "close_monitor*"} 
         | @@{command "declare_reference*"} 
-       ) '[' meta_args ']' 
-     ) 
+     ) '[' meta_args ']' 
      | change_status_command
      | inspection_command
      | macro_command
@@ -399,23 +406,35 @@ in the context of the SML toplevel of the Isabelle system as in the correspondin
 \<^theory_text>\<open>ML\<open> \<dots> SML-code \<dots> \<close>\<close>-command.
 \<close>
 
+(*<*)
+declare_reference*["text-elements-expls"::technical]
+(*>*)
+
 subsection\<open>Ontological Term-Contexts and their Management\<close>
 text\<open>The major commands providing term-contexts are 
-\<^theory_text>\<open>term*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close> and
-\<^theory_text>\<open>value*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close>\<^footnote>\<open>The meta-argument list is optional.\<close>.
+\<^theory_text>\<open>term*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close>,
+\<^theory_text>\<open>value*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close> and
+\<^theory_text>\<open>assert*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close>\<^footnote>\<open>The meta-argument list is optional.\<close>.
 Wrt. creation, track-ability and checking they are analogous to the ontological text and 
 code-commands. However the argument terms may contain term-antiquotations stemming from an
 ontology definition. Both term-contexts were type-checked and \<^emph>\<open>validated\<close> against
 the global context (so: in the term \<open>@{A \<open>oid\<close>}\<close>, \<open>oid\<close> is indeed a string which refers 
 to a meta-object belonging to the document class \<open>A\<close>, for example).
-The term-context in the \<open>value*\<close>-command is additionally expanded (\<^eg> replaced) by a term
-denoting the meta-object. This expansion happens \<^emph>\<open>before\<close> evaluation of the term, thus permitting
+The term-context in the \<open>value*\<close>-command and \<^emph>\<open>assert*\<close>-command is additionally expanded
+(\<^eg> replaced) by a term denoting the meta-object.
+This expansion happens \<^emph>\<open>before\<close> evaluation of the term, thus permitting
 executable HOL-functions to interact with meta-objects.
+The \<^emph>\<open>assert*\<close>-command allows for logical statements to be checked in the global context
+(see @{technical (unchecked) \<open>text-elements-expls\<close>}).
+% TODO:
+% Section reference @{docitem (unchecked) \<open>text-elements-expls\<close>} has not the right number
+This is particularly useful to explore formal definitions wrt. their border cases.
 
 Note unspecified attribute values were represented by free fresh variables which constrains \<^dof>
 to choose either the normalization-by-evaluation strategy \<^theory_text>\<open>nbe\<close> or a proof attempt via
 the \<^theory_text>\<open>auto\<close> method. A failure of these strategies will be reported and regarded as non-validation
 of this meta-object. The latter leads to a failure of the entire command.
+
 \<close>
 
 (*<*)
@@ -619,9 +638,6 @@ during the editing process but is only visible in the integrated source but usua
 a \<^typ>\<open>text_element\<close> to a specific \<^typ>\<open>author\<close>. Note that this is possible since \<^isadof> assigns to each
 document class also a class-type which is declared in the HOL environment.\<close>
 
-(*<*)
-declare_reference*["text-elements-expls"::example]
-(*>*)
 text*[s23::example, main_author = "Some(@{author \<open>bu\<close>})"]\<open>
 Recall that concrete authors can be denoted by term-antiquotations generated by \<^isadof>; for example,
 this may be for a text fragment like
@@ -649,7 +665,7 @@ of the \<^isadof> language:
        \<newline>
        '[' meta_args ']' '\<open>' text '\<close>'
      ) 
-     | @@{command "assert*"} '[' meta_args ']' '\<open>' term '\<close>'
+     
   \<close>
 \<close>
 
@@ -680,29 +696,28 @@ text\<open>
   \<^boxed_theory_text>\<open>title*\<open> ... \<close>\<close> or \<^boxed_theory_text>\<open>section*\<open> ... \<close>\<close>, \<^eg>:
 
 @{boxed_theory_text [display]\<open>
- title*[title::title]\<open>Isabelle/DOF\<close>
- subtitle*[subtitle::subtitle]\<open>User and Implementation Manual\<close>
- author*[adb::author, email="\<open>a.brucker@exeter.ac.uk\<close>",
-         orcid="\<open>0000-0002-6355-1200\<close>", http_site="\<open>https://brucker.ch/\<close>",
-         affiliation="\<open>University of Exeter, Exeter, UK\<close>"] \<open>Achim D. Brucker\<close>
- author*[bu::author, email = "\<open>wolff@lri.fr\<close>",
-         affiliation = "\<open>Université Paris-Saclay, LRI, Paris, France\<close>"]\<open>Burkhart Wolff\<close>
-\<close>}
+title*[title::title]\<open>Isabelle/DOF\<close>
+subtitle*[subtitle::subtitle]\<open>User and Implementation Manual\<close>
+author*[adb::author, email="\<open>a.brucker@exeter.ac.uk\<close>",
+        orcid="\<open>0000-0002-6355-1200\<close>", http_site="\<open>https://brucker.ch/\<close>",
+        affiliation="\<open>University of Exeter, Exeter, UK\<close>"] \<open>Achim D. Brucker\<close>
+author*[bu::author, email = "\<open>wolff@lri.fr\<close>",
+         affiliation = "\<open>Université Paris-Saclay, LRI, Paris, France\<close>"]\<open>Burkhart Wolff\<close>\<close>}
 
 \<close>
 
 text\<open>Assertions allow for logical statements to be checked in the global context.
-This is particularly useful to explore formal definitions wrt. their border cases. \<close>
-
-assert*[ass1::assertion, short_name = "\<open>This is an assertion\<close>"] \<open>last [3] < (4::int)\<close>
+This is particularly useful to explore formal definitions wrt. their border cases.
+@{boxed_theory_text [display]\<open>
+assert*[ass1::assertion, short_name = "\<open>This is an assertion\<close>"] \<open>last [3] < (4::int)\<close>\<close>}
+\<close>
 
 text\<open>We want to check the consequences of this definition and can add the following statements:
 @{boxed_theory_text [display]\<open>
 text*[claim::assertion]\<open>For non-empty lists, our definition yields indeed 
                                the last element of a list.\<close>
 assert*[claim1::assertion] \<open>last[4::int] = 4\<close>    
-assert*[claim2::assertion] \<open>last[1,2,3,4::int] = 4\<close>
-\<close>}
+assert*[claim2::assertion] \<open>last[1,2,3,4::int] = 4\<close>\<close>}
 \<close>
 
 text\<open>
@@ -714,14 +729,12 @@ However, in order to avoid the somewhat tedious consequence:
 
 the choice of the default class can be influenced by setting globally an attribute such as
 @{boxed_theory_text [display]
-\<open>declare[[ Definition_default_class = "definition"]]
- declare[[ Theorem_default_class    = "theorem"]]
-\<close>}
+\<open>declare[[Definition_default_class = "definition"]]
+declare[[Theorem_default_class = "theorem"]]\<close>}
 
 which allows the above example be shortened to:
 @{boxed_theory_text [display]
-\<open>Theorem*[T1, short_name="\<open>DF definition captures deadlock-freeness\<close>"]  \<open> \<dots> \<close>
-\<close>}
+\<open>Theorem*[T1, short_name="\<open>DF definition captures deadlock-freeness\<close>"]  \<open> \<dots> \<close>\<close>}
 \<close>
 
 subsection\<open>The Ontology \<^verbatim>\<open>technical_report\<close>\<close>
@@ -993,12 +1006,9 @@ text\<open>
   entities, \<^eg>, \<^ML_type>\<open>term\<close> (\<open>\<lambda>\<close>-term), \<^ML_type>\<open>typ\<close>, or
    \<^ML_type>\<open>thm\<close>, we represent the types of the implementation language
   \<^emph>\<open>inside\<close> the HOL type system.  We do, however, not reflect the data of
-  these types. They are just declared abstract types, 
-  ``inhabited'' by special constant symbols carrying strings, for
+  these types. They are just types declared in HOL, 
+  which are ``inhabited'' by special constant symbols carrying strings, for
   example of the format \<^boxed_theory_text>\<open>@{thm <string>}\<close>.
-  % TODO:
-  % Update meta-types implementation explanation to the new implementation
-  % in repository commit 08c101c5440eee2a087068581952026e88c39f6a
   When HOL
   expressions were used to denote values of \<^boxed_theory_text>\<open>doc_class\<close>
   instance attributes, this requires additional checks after
@@ -1226,12 +1236,11 @@ section*[infrastructure::technical]\<open>Technical Infrastructure\<close>
 text\<open> 
   The list of fully supported (\<^ie>, supporting both interactive ontological modeling and 
   document generation) ontologies and the list of supported document templates can be 
-  obtained by calling \<^boxed_bash>\<open>isabelle mkroot_DOF -h\<close> (see \<^technical>\<open>first_project\<close>).
+  obtained by calling \<^boxed_bash>\<open>isabelle dof_mkroot -h\<close> (see \<^technical>\<open>first_project\<close>).
   Note that the postfix \<^boxed_bash>\<open>-UNSUPPORTED\<close> denotes experimental ontologies or templates 
   for which further manual setup steps might be required or that are not fully tested. Also note 
   that the \<^LaTeX>-class files required by the templates need to be already installed on your 
-  system. This is mostly a problem for publisher specific templates (\<^eg>, Springer's 
-  \<^path>\<open>llncs.cls\<close>), which cannot be re-distributed due to copyright restrictions.
+  system. This is mostly a problem for publisher specific templates, which cannot be re-distributed due to copyright restrictions.
 \<close>
 
 subsection\<open>Developing Ontologies and their Representation Mappings\<close>
@@ -1282,9 +1291,9 @@ text\<open>
     file \<^path>\<open>src/ontologies/foo/DOF-foo.sty\<close>
   \<^item> registration (as import) of the new ontology in the file \<^path>\<open>src/ontologies/ontologies.thy\<close>. 
   \<^item> activation of the new document setup by executing the install script. You can skip the lengthy 
-    checks for the AFP entries by using the 
-    \<^boxed_bash>\<open>--skip-patch-and-afp\<close> option:
-    @{boxed_bash [display] \<open>ë\prompt{\isadofdirn}ë ./install --skip-patch-and-afp\<close>}
+    checks for the AFP entries and the installation of the Isabelle patch by using the 
+    \<^boxed_bash>\<open>--skip-afp\<close> option:
+    @{boxed_bash [display] \<open>ë\prompt{\isadofdirn}ë ./install --skip-afp\<close>}
 \<close>
 
 subsection\<open>Document Templates\<close>
@@ -1313,8 +1322,8 @@ text\<open>
   \<^item> develop a new \<^LaTeX>-template \<^boxed_bash>\<open>src/document-templates/root-bar.tex\<close>
   \<^item> activation of the new document template  by executing the \<^boxed_bash>\<open>install\<close> script. You can skip the lengthy 
     checks for the AFP entries and the installation of the Isabelle patch by using the 
-    \<^boxed_bash>\<open>--skip-patch-and-afp\<close> option:
-    @{boxed_bash [display] \<open>ë\prompt{\isadofdirn}ë ./install --skip-patch-and-afp\<close>}
+    \<^boxed_bash>\<open>--skip-afp\<close> option:
+    @{boxed_bash [display] \<open>ë\prompt{\isadofdirn}ë ./install --skip-afp\<close>}
 \<close>
 
 
@@ -1351,14 +1360,7 @@ text\<open>
 \usepackage{isabelle,isabellesym,amssymb} % Required (by Isabelle)
 \usepackage{amsmath}           % Used by some ontologies  
 \bibliographystyle{abbrv}
-\IfFileExists{DOF-core.sty}{}{ % Required by Isabelle/DOF
-  \PackageError{DOF-core}{The doëëcument preparation 
-   requires the Isabelle/DOF framework.}{For further help, see 
-   ë\url{\dofurl}ë
-}
-\input{ontologies}             % This will include the document specific 
-                               % ontologies from isadof.cfg
-\IfFileExists{preamble.tex}{\input{preamble.tex}}{}  
+\input{dof-common} % setup shared between all Isabelle/DOF templates
 \usepackage{graphicx}          % Required for images. 
 \usepackage[caption]{subfig}
 \usepackage[size=footnotesize]{caption}
@@ -1384,7 +1386,7 @@ text\<open>
 
 subsubsection\<open>Getting Started\<close>
 text\<open>
-  In general, we recommend creating a test project (\<^eg>, using \<^boxed_bash>\<open>isabelle mkroot_DOF\<close>)
+  In general, we recommend creating a test project (\<^eg>, using \<^boxed_bash>\<open>isabelle dof_mkroot\<close>)
   to develop new document templates or ontology representations. The default setup of the \<^isadof>
   build system generated a \<^path>\<open>output/document\<close> directory with a self-contained \<^LaTeX>-setup. In 
   this directory, you can directly use \<^LaTeX> on the main file, called \<^path>\<open>root.tex\<close>:

examples/technical_report/Isabelle_DOF-Manual/ROOT

@@ -1,13 +1,13 @@
 session "Isabelle_DOF-Manual" = "Isabelle_DOF" + 
-  options  [document = pdf, document_output = "output", quick_and_dirty = true]
+  options  [document = pdf, document_output = "output", document_build = dof,
+    dof_ontologies = "Isabelle_DOF.technical_report Isabelle_DOF.cenelec_50128", dof_template = "Isabelle_DOF.scrreprt-modern",
+    quick_and_dirty = true]
   theories
     "Isabelle_DOF-Manual"
   document_files
-    "isadof.cfg"
     "root.bib"
     "root.mst"
     "preamble.tex"
-    "build"
     "lstisadof-manual.sty" 
     "figures/antiquotations-PIDE.png"
     "figures/cicm2018-combined.png"

examples/technical_report/Isabelle_DOF-Manual/document/build

@@ -1,46 +0,0 @@
-#!/usr/bin/env bash
-# Copyright (c) 2018-2019 The University of Sheffield. All rights reserved.
-#               2018 The University of Paris-Saclay. All rights reserved.
-#
-# 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
-    echo ""
-    echo "Error: Isabelle/DOF not installed"
-    echo "====="
-    echo "This is a Isabelle/DOF project. The document preparation requires"
-    echo "the Isabelle/DOF framework. Please obtain the framework by cloning"
-    echo "the Isabelle/DOF git repository, i.e.: "
-    echo "    git clone https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF"
-    echo "You can install the framework as follows:"
-    echo "    cd Isabelle_DOF/document-generator"
-    echo "    ./install"
-    echo ""
-    exit 1
-fi
-
-cp $ISABELLE_HOME_USER/DOF/document-template/build_lib.sh .
-source build_lib.sh

examples/technical_report/Isabelle_DOF-Manual/document/isadof.cfg

@@ -1,4 +0,0 @@
-Template: scrreprt-modern
-Ontology: technical_report
-Ontology: cenelec_50128
-

examples/technical_report/TR_my_commented_isabelle/ROOT

@@ -1,13 +1,13 @@
 session "TR_MyCommentedIsabelle" = "Isabelle_DOF" +
-  options [document = pdf, document_output = "output",quick_and_dirty = true]
+  options [document = pdf, document_output = "output", document_build = dof,
+           dof_ontologies = "Isabelle_DOF.technical_report", dof_template = Isabelle_DOF.scrreprt,
+    quick_and_dirty = true]
   theories
     "TR_MyCommentedIsabelle"
   document_files
     "root.bib"
-    "isadof.cfg"
     "preamble.tex"
     "prooftree.sty"
-    "build"
     "figures/markup-demo.png"
     "figures/text-element.pdf"
     "figures/isabelle-architecture.pdf"

examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy

@@ -612,32 +612,36 @@ subsection\<open>More operations on types\<close>
 text\<open>
 \<^item> \<^ML>\<open>Term_Subst.map_types_same : (typ -> typ) -> term -> term\<close>
 \<^item> \<^ML>\<open>Term_Subst.map_aterms_same : (term -> term) -> term -> term\<close>
-\<^item> \<^ML>\<open>Term_Subst.instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list 
-                              -> term -> term\<close>
-\<^item> \<^ML>\<open>Term_Subst.instantiateT: ((indexname * sort) * typ) list -> typ -> typ\<close>
-\<^item> \<^ML>\<open>Term_Subst.generalizeT: string list -> int -> typ -> typ\<close>
+\<^item> \<^ML>\<open>Term_Subst.instantiate: typ TVars.table * term Vars.table -> term -> term\<close>
+\<^item> \<^ML>\<open>Term_Subst.instantiateT: typ TVars.table -> typ -> typ\<close>
+\<^item> \<^ML>\<open>Term_Subst.generalizeT: Names.set -> int -> typ -> typ\<close>
                         this is the standard type generalisation function !!!
                         only type-frees in the string-list were taken into account. 
-\<^item> \<^ML>\<open>Term_Subst.generalize: string list * string list -> int -> term -> term\<close>
+\<^item> \<^ML>\<open>Term_Subst.generalize: Names.set * Names.set -> int -> term -> term\<close>
                         this is the standard term generalisation function !!!
                         only type-frees and frees in the string-lists were taken 
                         into account. 
 \<close>
 
+
+
 text \<open>Apparently, a bizarre conversion between the old-style interface and 
   the new-style  \<^ML>\<open>tyenv\<close> is necessary. See the following example.\<close>
 ML\<open>
-val S = Vartab.dest tyenv;
+val S = Vartab.dest tyenv : (Vartab.key * (sort * typ)) list;
 val S' = (map (fn (s,(t,u)) => ((s,t),u)) S) : ((indexname * sort) * typ) list;
          (* it took me quite some time to find out that these two type representations,
             obscured by a number of type-synonyms, where actually identical. *)
+val S''= TVars.make S': typ TVars.table
 val ty = t_schematic;
-val ty' = Term_Subst.instantiateT S' t_schematic;
+val ty' = Term_Subst.instantiateT S'' t_schematic;
+
+(* Don't know how to build a typ TVars.table *)
 val t = (generalize_term @{term "[]"});
 
-val t' = Term_Subst.map_types_same (Term_Subst.instantiateT S') (t)
+val t' = Term_Subst.map_types_same (Term_Subst.instantiateT (TVars.make S')) (t)
 (* or alternatively : *)
-val t'' = Term.map_types (Term_Subst.instantiateT S') (t)
+val t'' = Term.map_types (Term_Subst.instantiateT S'') (t)
 \<close>
 
 text\<open>A more abstract env for variable management in tactic proofs. A bit difficult to use
@@ -794,11 +798,11 @@ text\<open> We come now to the very heart of the LCF-Kernel of Isabelle, which
 \<^item>  \<^ML>\<open> Thm.forall_intr: cterm -> thm -> thm\<close>
 \<^item>  \<^ML>\<open> Thm.forall_elim: cterm -> thm -> thm\<close>
 \<^item>  \<^ML>\<open> Thm.transfer : theory -> thm -> thm\<close>
-\<^item>  \<^ML>\<open> Thm.generalize: string list * string list -> int -> thm -> thm\<close>
-\<^item>  \<^ML>\<open> Thm.instantiate: ((indexname*sort)*ctyp)list * ((indexname*typ)*cterm) list -> thm -> thm\<close>
+\<^item>  \<^ML>\<open> Thm.generalize: Names.set * Names.set -> int -> thm -> thm\<close>
+\<^item>  \<^ML>\<open> Thm.instantiate: ctyp TVars.table * cterm Vars.table -> thm -> thm\<close>
 \<close>
 
-text\<open>  They reflect the Pure logic depicted in a number of presentations such as 
+text\<open>  They reflect the Pure logic depicted in a number of presentations such as
   M. Wenzel, \<^emph>\<open>Parallel Proof Checking in Isabelle/Isar\<close>, PLMMS 2009, or simiular papers.
   Notated as logical inference rules, these operations were presented as follows:
 \<close>
@@ -909,14 +913,10 @@ high-level component (more low-level components such as \<^ML>\<open>Global_Theo
 exist) for definitions and axiomatizations is here:
 \<close>
 
-
 text\<open>
 \<^item>  \<^ML>\<open>Specification.definition: (binding * typ option * mixfix) option ->
         (binding * typ option * mixfix) list -> term list -> Attrib.binding * term ->
         local_theory -> (term * (string * thm)) * local_theory\<close>
-\<^item>  \<^ML>\<open>Specification.definition': (binding * typ option * mixfix) option ->
-        (binding * typ option * mixfix) list ->  term list -> Attrib.binding * term ->
-        bool -> local_theory -> (term * (string * thm)) * local_theory\<close>
 \<^item>  \<^ML>\<open>Specification.definition_cmd: (binding * string option * mixfix) option ->
         (binding * string option * mixfix) list -> string list -> Attrib.binding * string ->
          bool -> local_theory -> (term * (string * thm)) * local_theory\<close>
@@ -959,8 +959,8 @@ fun mk_def name p  =
         val ty_global = ty --> ty
         val args = (((SOME(nameb,SOME ty_global,NoSyn),(Binding.empty_atts,term_prop)),[]),[])
         val cmd = (fn (((decl, spec), prems), params) =>
-                        #2 oo Specification.definition' decl params prems spec)
-    in cmd args true
+                        #2 o Specification.definition decl params prems spec)
+    in cmd args
     end;
 in  Named_Target.theory_map (mk_def "I" @{here} )
 end\<close>
@@ -1186,8 +1186,8 @@ text\<open> The extensibility of Isabelle as a system framework depends on a num
  \<^item> \<^ML>\<open>Toplevel.theory': (bool -> theory -> theory) -> Toplevel.transition -> Toplevel.transition\<close>
  \<^item> \<^ML>\<open>Toplevel.exit: Toplevel.transition -> Toplevel.transition\<close>
  \<^item> \<^ML>\<open>Toplevel.ignored: Position.T -> Toplevel.transition\<close>
- \<^item> \<^ML>\<open>Toplevel.present_local_theory: (xstring * Position.T) option ->
-                       (Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition\<close>
+ \<^item> \<^ML>\<open>Toplevel.present_local_theory:  (xstring * Position.T) option ->
+                       (Toplevel.state -> Latex.text) -> Toplevel.transition -> Toplevel.transition\<close>
 
 \<close>
 subsection*[cmdbinding::technical] \<open>Toplevel Transaction Management in the Isar-Engine\<close>
@@ -1216,32 +1216,45 @@ text\<open>
 
 text\<open>The file \<^file>\<open>~~/src/HOL/Examples/Commands.thy\<close> shows some example Isar command definitions, with the 
      all-important theory header declarations for outer syntax keywords.\<close>
+ 
+text\<open>@{ML_structure Pure_Syn}\<close>
 
 subsubsection*[ex1137::example]\<open>Examples: \<^theory_text>\<open>text\<close>\<close>
 text\<open> The integration of the  \<^theory_text>\<open>text\<close>-command is done as follows:
 
  @{ML [display]\<open>
   Outer_Syntax.command ("text", @{here}) "formal comment (primary style)"
-    (Parse.opt_target -- Parse.document_source >> Pure_Syn.document_command {markdown = true})
+    (Parse.opt_target -- Parse.document_source >> Document_Output.document_output 
+                                                  {markdown = true, markup = I})
  \<close>}
 
- where \<^ML>\<open>Pure_Syn.document_command\<close> is the defining operation for the 
- "diagnostic" (=side-effect-free) toplevel operation. \<^ML>\<open>Pure_Syn.document_command\<close> looks as follows:
+ where \<^ML>\<open>Document_Output.document_output\<close> is the defining operation for the 
+ "diagnostic" (=side-effect-free) toplevel operation.
+  \<^ML>\<open>Document_Output.document_output\<close> looks as follows:
 
- @{ML [display]\<open> let fun output_document state markdown txt = 
-                           Thy_Output.output_document (Toplevel.presentation_context state) markdown txt
-                     fun document_command markdown (loc, txt) =
-  Toplevel.keep (fn state =>
-    (case loc of
-      NONE => ignore (output_document state markdown txt)
-    | SOME (_, pos) => 
-        error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o
-        Toplevel.present_local_theory loc (fn state =>
-              ignore (output_document state markdown txt)) in () end
-   
+ @{ML [display]\<open>let fun document_reports txt =
+  let val pos = Input.pos_of txt in
+    [(pos, Markup.language_document (Input.is_delimited txt)),
+     (pos, Markup.plain_text)]
+  end;
+fun document_output {markdown, markup} (loc, txt) =
+  let
+    fun output st =
+      let
+        val ctxt = Toplevel.presentation_context st;
+        val _ = Context_Position.reports ctxt (document_reports txt);
+      in txt |> Document_Output.output_document ctxt {markdown = markdown} |> markup end;
+  in
+    Toplevel.present (fn st =>
+      (case loc of
+        NONE => output st
+      | SOME (_, pos) =>
+          error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o
+    Toplevel.present_local_theory loc output
+  end in () end
 \<close>}
-
 \<close>
+
 subsubsection*[ex1138::example]\<open>Examples: \<^theory_text>\<open>ML\<close>\<close>
 
 text\<open>
@@ -1316,10 +1329,12 @@ subsection*[ex213::example]\<open>A Definition Command (High-level)\<close>
 
 text\<open>A quite complex example is drawn from the Theory \<^verbatim>\<open>Clean\<close>; it generates \<close>
 
+ML\<open>Specification.definition\<close>
+
 ML\<open>
 structure HLDefinitionSample = 
 struct
-fun cmd (decl, spec, prems, params) = #2 oo Specification.definition' decl params prems spec
+fun cmd (decl, spec, prems, params) = #2 o Specification.definition decl params prems spec
 
 fun MON_SE_T res state = state --> optionT(HOLogic.mk_prodT(res,state));
 
@@ -1340,7 +1355,7 @@ fun mk_push_def binding sty lthy =
         val eq = push_eq binding  (Binding.name_of name) rty sty lthy
         val mty = MON_SE_T rty sty 
         val args = (SOME(name, SOME mty, NoSyn), (Binding.empty_atts,eq),[],[])
-    in cmd args true lthy  end;
+    in cmd args lthy  end;
 
 val define_test =  Named_Target.theory_map (mk_push_def (Binding.name "test") @{typ "'a"})
 
@@ -1536,6 +1551,7 @@ text\<open>The structures @{ML_structure Markup} and @{ML_structure Properties}
   from \<^theory_text>\<open>Isabelle_DOF\<close>. A markup must be tagged with an id; this is done by the @{ML serial}-function
   discussed earlier. Markup operations were used for hyperlinking applications to binding
   occurrences, info for hovering, infos for type ... \<close>  
+
 ML\<open>
 (* Position.report is also a type consisting of a pair of a position and markup. *)
 (* It would solve all my problems if I find a way to infer the defining Position.report
@@ -1551,20 +1567,18 @@ Markup.enclose : Markup.T -> string -> string;
      
 (* example for setting a link, the def flag controls if it is a defining or a binding 
 occurence of an item *)
-fun theory_markup (def:bool) (name:string) (id:serial) (pos:Position.T) =
-  if id = 0 then Markup.empty
-  else
-    Markup.properties (Position.entity_properties_of def id pos)
-      (Markup.entity Markup.theoryN name);
 Markup.theoryN : string;
 
+fun theory_markup refN  (def:bool) (name:string) (id:serial) (pos:Position.T) =
+  if id = 0 then Markup.empty
+  else Position.make_entity_markup {def = def} id refN (name, pos);
+
 serial();   (* A global, lock-guarded serial counter used to produce unique identifiers,
                be it on the level of thy-internal states or as reference in markup in
                PIDE *)
 \<close>
 
 
-
 subsection\<open>A simple Example\<close>
 ML\<open>
 local 
@@ -1573,10 +1587,7 @@ val docclassN = "doc_class";
 
 (* derived from: theory_markup; def for "defining occurrence" (true) in contrast to
    "referring occurence" (false). *) 
-fun docclass_markup def name id pos =
-  if id = 0 then Markup.empty
-  else           Markup.properties (Position.entity_properties_of def id pos)
-                                   (Markup.entity docclassN name);   
+val docclass_markup  = theory_markup docclassN  
 
 in
 
@@ -1602,14 +1613,16 @@ fun markup_tvar def_name ps (name, id) =
   let 
     fun markup_elem name = (name, (name, []): Markup.T);
     val (tvarN, tvar) = markup_elem ((case def_name of SOME name => name | _ => "") ^ "'s nickname is");
-    val entity = Markup.entity tvarN name
+    val entity = Markup.entity tvarN name (* ??? *)
     val def = def_name = NONE
   in
     tvar ::
     (if def then I else cons (Markup.keyword_properties Markup.ML_keyword3))
-      (map (fn pos => Markup.properties (Position.entity_properties_of def id pos) entity) ps)
+      (map (fn pos => Position.make_entity_markup {def = def} id tvarN (name, pos) ) ps)
   end
 
+(* Position.make_entity_markup {def = def} id refN (name, pos) *)
+
 fun report [] _ _ = I
   | report ps markup x =
       let val ms = markup x
@@ -1856,11 +1869,6 @@ Common Isar Syntax
 
 
 Common Isar Syntax
-\<^item>\<^ML>\<open>Args.embedded_token  : Token.T parser\<close>
-\<^item>\<^ML>\<open>Args.embedded_inner_syntax: string parser\<close>
-\<^item>\<^ML>\<open>Args.embedded_input  : Input.source parser\<close>
-\<^item>\<^ML>\<open>Args.embedded  : string parser\<close>
-\<^item>\<^ML>\<open>Args.embedded_position: (string * Position.T) parser\<close>
 \<^item>\<^ML>\<open>Args.text_input: Input.source parser\<close>
 \<^item>\<^ML>\<open>Args.text      : string parser\<close>
 \<^item>\<^ML>\<open>Args.binding   : Binding.binding parser\<close>
@@ -2058,6 +2066,10 @@ text\<open>
 
 
 
+(*
+Document_Antiquotation
+*)
+
 subsection*[ex33::example] \<open>Example\<close>
 
 ML\<open>
@@ -2070,10 +2082,10 @@ ML\<open>
      
      (* Here is the code to register the above parsers as text antiquotations into the Isabelle
         Framework: *)
-     Thy_Output.antiquotation_pretty_source \<^binding>\<open>theory\<close> 
-                                            (Scan.lift (Parse.position Args.embedded));
+      Document_Output.antiquotation_pretty_source \<^binding>\<open>theory\<close> 
+                                            (Scan.lift (Parse.position Parse.embedded));
      
-     Thy_Output.antiquotation_raw           \<^binding>\<open>file\<close> 
+      Document_Output.antiquotation_raw           \<^binding>\<open>file\<close> 
                                             (Scan.lift (Parse.position Parse.path))  ;
      
 \<close>
@@ -2084,7 +2096,7 @@ text\<open>where we have the registration of the action
      transaction that, of course, has the type \<^ML_type>\<open>theory -> theory\<close> :
 
      @{ML [display] \<open>
-          (fn name => (Thy_Output.antiquotation_pretty_source 
+          (fn name => (Document_Output.antiquotation_pretty_source 
                  name
                 (Scan.lift (Parse.position Args.cartouche_input))))
           : binding -> 
@@ -2104,7 +2116,7 @@ ML\<open> Output.output "bla_1:" \<close>
 text\<open>It provides a number of hooks that can be used for redirection hacks ...\<close>
 
 section \<open> Output: LaTeX \<close>
-text\<open>The heart of the LaTeX generator is to be found in the structure \<^ML_structure>\<open>Thy_Output\<close>.
+text\<open>The heart of the LaTeX generator is to be found in the structure \<^ML_structure>\<open>Document_Output\<close>.
 This is an own parsing and writing process, with the risc that a parsed file in the IDE parsing
 process can not be parsed for the LaTeX Generator. The reason is twofold:
 
@@ -2120,60 +2132,52 @@ Since Isabelle2018, an own AST is provided for the LaTeX syntax, analogously to
 \<^item>\<^ML>\<open>Latex.string: string -> Latex.text\<close>
 \<^item>\<^ML>\<open>Latex.text: string * Position.T -> Latex.text\<close>
 
-\<^item>\<^ML>\<open>Latex.output_text: Latex.text list -> string\<close>
-\<^item>\<^ML>\<open>Latex.output_positions: Position.T -> Latex.text list -> string\<close>
 \<^item>\<^ML>\<open>Latex.output_name: string -> string\<close>
 \<^item>\<^ML>\<open>Latex.output_ascii: string -> string\<close>
 \<^item>\<^ML>\<open>Latex.output_symbols: Symbol.symbol list -> string\<close>
                                                                           
-\<^item>\<^ML>\<open>Latex.begin_delim: string -> string\<close>
-\<^item>\<^ML>\<open>Latex.end_delim: string -> string\<close>
-\<^item>\<^ML>\<open>Latex.begin_tag: string -> string\<close>
-\<^item>\<^ML>\<open>Latex.end_tag: string -> string\<close>
-\<^item>\<^ML>\<open>Latex.environment_block: string -> Latex.text list -> Latex.text\<close>
-\<^item>\<^ML>\<open>Latex.environment: string -> string -> string\<close>
 
-\<^item>\<^ML>\<open>Latex.block: Latex.text list -> Latex.text\<close>
-\<^item>\<^ML>\<open>Latex.enclose_body: string -> string -> Latex.text list -> Latex.text list\<close>
-\<^item>\<^ML>\<open>Latex.enclose_block: string -> string -> Latex.text list -> Latex.text\<close>
+\<^item>\<^ML>\<open>Latex.environment: string -> Latex.text -> Latex.text\<close>
+
+\<^item>\<^ML>\<open>Latex.block: Latex.text -> XML.tree\<close>
 \<close>
 
 
 
 ML\<open> Latex.output_ascii;
-    Latex.environment "isa" "bg";
+    Latex.environment "isa" (Latex.string "bg");
     Latex.output_ascii "a_b:c'é";
     (* Note: *)
     space_implode "sd &e sf dfg" ["qs","er","alpa"]; 
   \<close>
 
-text\<open>Here is an abstract of the main interface to @{ML_structure Thy_Output}:\<close>
+text\<open>Here is an abstract of the main interface to @{ML_structure Document_Output}:\<close>
 
 text\<open>
-\<^item>\<^ML>\<open>Thy_Output.output_document: Proof.context -> {markdown: bool} -> Input.source -> Latex.text list\<close>
-\<^item>\<^ML>\<open>Thy_Output.output_token: Proof.context -> Token.T -> Latex.text list\<close>
-\<^item>\<^ML>\<open>Thy_Output.output_source: Proof.context -> string -> Latex.text list\<close>
-\<^item>\<^ML>\<open>Thy_Output.present_thy: Options.T -> theory -> Thy_Output.segment list -> Latex.text list\<close>
+\<^item>\<^ML>\<open>Document_Output.output_document: Proof.context -> {markdown: bool} -> Input.source -> Latex.text \<close>
+\<^item>\<^ML>\<open>Document_Output.output_token: Proof.context -> Token.T -> Latex.text \<close>
+\<^item>\<^ML>\<open>Document_Output.output_source: Proof.context -> string -> Latex.text \<close>
+\<^item>\<^ML>\<open>Document_Output.present_thy: Options.T -> theory -> Document_Output.segment list -> Latex.text \<close>
 
-\<^item>\<^ML>\<open>Thy_Output.isabelle: Proof.context -> Latex.text list -> Latex.text\<close>
-\<^item>\<^ML>\<open>Thy_Output.isabelle_typewriter: Proof.context -> Latex.text list -> Latex.text\<close>
-\<^item>\<^ML>\<open>Thy_Output.typewriter: Proof.context -> string -> Latex.text\<close>
-\<^item>\<^ML>\<open>Thy_Output.verbatim: Proof.context -> string -> Latex.text\<close>
-\<^item>\<^ML>\<open>Thy_Output.source: Proof.context -> {embedded: bool} -> Token.src -> Latex.text\<close>
-\<^item>\<^ML>\<open>Thy_Output.pretty: Proof.context -> Pretty.T -> Latex.text\<close>
-\<^item>\<^ML>\<open>Thy_Output.pretty_source: Proof.context -> {embedded: bool} -> Token.src -> Pretty.T -> Latex.text\<close>
-\<^item>\<^ML>\<open>Thy_Output.pretty_items: Proof.context -> Pretty.T list -> Latex.text\<close>
-\<^item>\<^ML>\<open>Thy_Output.pretty_items_source: Proof.context -> {embedded: bool} -> Token.src -> Pretty.T list -> Latex.text\<close>
+\<^item>\<^ML>\<open>Document_Output.isabelle: Proof.context -> Latex.text  -> Latex.text\<close>
+\<^item>\<^ML>\<open>Document_Output.isabelle_typewriter: Proof.context -> Latex.text  -> Latex.text\<close>
+\<^item>\<^ML>\<open>Document_Output.typewriter: Proof.context -> string -> Latex.text\<close>
+\<^item>\<^ML>\<open>Document_Output.verbatim: Proof.context -> string -> Latex.text\<close>
+\<^item>\<^ML>\<open>Document_Output.source: Proof.context -> {embedded: bool} -> Token.src -> Latex.text\<close>
+\<^item>\<^ML>\<open>Document_Output.pretty: Proof.context -> Pretty.T -> Latex.text\<close>
+\<^item>\<^ML>\<open>Document_Output.pretty_source: Proof.context -> {embedded: bool} -> Token.src -> Pretty.T -> Latex.text\<close>
+\<^item>\<^ML>\<open>Document_Output.pretty_items: Proof.context -> Pretty.T list -> Latex.text\<close>
+\<^item>\<^ML>\<open>Document_Output.pretty_items_source: Proof.context -> {embedded: bool} -> Token.src -> Pretty.T list -> Latex.text\<close>
 
 Finally a number of antiquotation registries :
 
-\<^item>\<^ML>\<open>Thy_Output.antiquotation_pretty:
+\<^item>\<^ML>\<open>Document_Output.antiquotation_pretty:
                  binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory\<close>
-\<^item>\<^ML>\<open>Thy_Output.antiquotation_pretty_source:
+\<^item>\<^ML>\<open>Document_Output.antiquotation_pretty_source:
                  binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory\<close>
-\<^item>\<^ML>\<open>Thy_Output.antiquotation_raw:
+\<^item>\<^ML>\<open>Document_Output.antiquotation_raw:
                  binding -> 'a context_parser -> (Proof.context -> 'a -> Latex.text) -> theory -> theory\<close>
-\<^item>\<^ML>\<open>Thy_Output.antiquotation_verbatim:
+\<^item>\<^ML>\<open>Document_Output.antiquotation_verbatim:
                binding -> 'a context_parser -> (Proof.context -> 'a -> string) -> theory -> theory\<close>
 \<close>
 

examples/technical_report/TR_my_commented_isabelle/document/build

@@ -1,46 +0,0 @@
-#!/usr/bin/env bash
-# Copyright (c) 2018-2019 The University of Sheffield. All rights reserved.
-#               2018 The University of Paris-Saclay. All rights reserved.
-#
-# 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
-    echo ""
-    echo "Error: Isabelle/DOF not installed"
-    echo "====="
-    echo "This is a Isabelle/DOF project. The document preparation requires"
-    echo "the Isabelle/DOF framework. Please obtain the framework by cloning"
-    echo "the Isabelle/DOF git repository, i.e.: "
-    echo "    git clone https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF"
-    echo "You can install the framework as follows:"
-    echo "    cd Isabelle_DOF/document-generator"
-    echo "    ./install"
-    echo ""
-    exit 1
-fi
-
-cp $ISABELLE_HOME_USER/DOF/document-template/build_lib.sh .
-source build_lib.sh