Merge branch 'master' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF

.ci/mk_release

@@ -26,7 +26,7 @@
 #
 # SPDX-License-Identifier: BSD-2-Clause
 
-#set -e
+set -e
 shopt -s nocasematch
 
 
@@ -84,18 +84,30 @@ clone_repo()
     
 }
 
-build_and_install_manual()
+build_and_install_manuals()
 {
     echo "* Building manual"
     ROOTS=$ISABELLE_HOME_USER/ROOTS
     if [ -f $ROOTS ]; then
         mv $ROOTS $ROOTS.backup
     fi
+
     (cd $ISADOF_WORK_DIR && ./install)
+
+    echo "Isabelle/DOF Manuals!" > $ISADOF_WORK_DIR/doc/Contents
+    
     (cd $ISADOF_WORK_DIR && $ISABELLE build -c Isabelle_DOF-Manual)
     mkdir -p $ISADOF_WORK_DIR/doc
     cp $ISADOF_WORK_DIR/examples/technical_report/Isabelle_DOF-Manual/output/document.pdf \
         $ISADOF_WORK_DIR/doc/Isabelle_DOF-Manual.pdf
+    echo "  Isabelle_DOF-Manual                       User and Implementation Manual for Isabelle/DOF" >> $ISADOF_WORK_DIR/doc/Contents
+
+    (cd $ISADOF_WORK_DIR && $ISABELLE build -c 2018-cicm-isabelle_dof-applications)
+    mkdir -p $ISADOF_WORK_DIR/doc
+    cp $ISADOF_WORK_DIR/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/output/document.pdf \
+        $ISADOF_WORK_DIR/doc/2018-cicm-isabelle_dof-applications.pdf
+    echo "  2018-cicm-isabelle_dof-applications       Example academic paper" >> $ISADOF_WORK_DIR/doc/Contents
+
     find $ISADOF_WORK_DIR -type d -name "output" -exec rm -rf {} \; &> /dev/null || true
     rm -rf $ISADOF_WORK_DIR/.git* $ISADOF_WORK_DIR/.ci $ISADOF_WORK_DIR/.afp 
     if [ -f $ROOTS.backup ]; then
@@ -171,7 +183,7 @@ for i in $VARS; do
         export "$i"
 done
 
-build_and_install_manual
+build_and_install_manuals
 
 create_archive
 

install

@@ -235,6 +235,13 @@ install_and_register(){
         echo 'ISABELLE_TOOLS=$ISABELLE_TOOLS:$ISABELLE_HOME_USER/DOF/Tools' \
              >> "$DIR/settings"
     fi
+    if [[ $ISABELLE_DOCS = *DOF* ]]; then
+        echo "    * Docs already registered in $DIR/settings"
+    else
+        echo "    * Registering docs in $DIR/settings"
+        echo "ISABELLE_DOCS=$PWD/doc"':$ISABELLE_DOCS' \
+             >> "$DIR/settings"
+    fi
     sed -i -e "s|<isadofurl>|$DOF_URL|" $ISABELLE_HOME_USER/DOF/*/*
     LTX_VERSION="$DATE $DOF_VERSION/$ISABELLE_SHORT_VERSION"
     sed -i -e "s|<isadofltxversion>|$LTX_VERSION|" $ISABELLE_HOME_USER/DOF/*/*

src/DOF/RegExpChecker.sml

@@ -1,3 +1,16 @@
+(*************************************************************************
+ * Copyright (C) 
+ *               2019      The University of Exeter 
+ *               2018-2019 The University of Paris-Saclay
+ *               2018      The University of Sheffield
+ *
+ * License:
+ *   This program can be redistributed and/or modified under the terms
+ *   of the 2-clause BSD-style license.
+ *
+ *   SPDX-License-Identifier: BSD-2-Clause
+ *************************************************************************)
+
 structure RegExpChecker : sig
   type 'a equal
   type num