Split ontologies from templates - they can now be configured separately.

document-generator/Tools/DOF_mkroot

@@ -41,8 +41,15 @@ function usage()
   echo "    -h           print this help text and exit"
   echo "    -d           enable document preparation"
   echo "    -n NAME      alternative session name (default: DIR base name)"
-  echo "    -o TEMPLATE  alternative setup for root.tex (default: basic support using scrreprt)"
-  echo "       Available templates:"
+  echo "    -o ONTOLOGY  (default: $DEFAULT_ONTOLOGY)"
+  echo "       Available ontologies:"
+  for t in "$ISABELLE_HOME_USER/DOF/latex/"*.sty; do
+    if [[ $t =~ DOF-(.*).sty$ ]]; then
+      echo "       * ${BASH_REMATCH[1]}"
+    fi
+  done
+  echo "    -t TEMPLATE   (default: DEFAULT_TEMPLATE)"
+  echo "       Available document templates:"
   for t in "$ISABELLE_HOME_USER/DOF/document-template/"*.tex; do
     if [[ $t =~ root-(.*).tex$ ]]; then
       echo "       * ${BASH_REMATCH[1]}"
@@ -67,9 +74,13 @@ function fail()
 
 DOC=""
 NAME=""
-TEMPLATE="default-scrreprt"
+DEFAULT_TEMPLATE="scrreprt"
+DEFAULT_ONTOLOGY="core"
 
-while getopts "o:n:dh" OPT
+TEMPLATE="$DEFAULT_TEMPLATE"
+ONTOLOGY="$DEFAULT_ONTOLOGY"
+
+while getopts "t:o:n:dh" OPT
 do
   case "$OPT" in
     h)
@@ -83,7 +94,18 @@ do
       NAME="$OPTARG"
       ;;
     o)
+      if [ ! -f "$ISABELLE_HOME_USER/DOF/latex/DOF-$OPTARG.sty" ]; then
+          echo "ERROR: Ontology $OPTARG not available!"
+          exit 1
+      fi
+      ONTOLOGY="$ONTOLOGY $OPTARG"
+      ;;
+    t)
       TEMPLATE="$OPTARG"
+      if [ ! -f "$ISABELLE_HOME_USER/DOF/document-template/root-$TEMPLATE.tex" ]; then
+          echo "ERROR: Template $TEMPLATE not available!"
+          exit 1
+      fi
       ;;
     \?)
       usage
@@ -113,11 +135,16 @@ fi
 if [ "$DOC" = true ]; then
   $ISABELLE_TOOL mkroot -d -n "$NAME" "$DIR"
   echo "    \"preamble.tex\"" >> "$DIR"/ROOT
+  echo "    \"ontologies.tex\"" >> "$DIR"/ROOT
   echo "    \"build\"" >> "$DIR"/ROOT
   TITLE=$(echo "$NAME" | tr _ - | tr -d '\\')
   AUTHOR=$(echo "By $USER" | tr _ - | tr -d '\\')
   cp "$ISABELLE_HOME_USER/DOF/document-template/build" "$DIR"/document/
   cp "$ISABELLE_HOME_USER/DOF/document-template/preamble.tex" "$DIR"/document/
+  cp "$ISABELLE_HOME_USER/DOF/document-template/ontologies.tex" "$DIR"/document/
+  for o in $ONTOLOGY; do
+    echo "\usepackage{$o}" >> "$DIR"/document/ontologies.tex;
+  done
   sed -e "s/<AUTHOR>/$AUTHOR/" -e "s/<TITLE>/$TITLE/" "$ISABELLE_HOME_USER/DOF/document-template/root-$TEMPLATE.tex" > "$DIR"/document/root.tex
 else
     $ISABELLE_TOOL mkroot -n "$NAME"

document-generator/document-template/ontologies.tex

@@ -0,0 +1,14 @@
+%% Copyright (C) 2018 The University of Sheffield
+%%               2018 The University of Paris-Sud
+%%
+%% 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 of the License, or any later version.
+%%   OR
+%%   The 2-clause BSD-style license.
+%%  
+%%   SPDX-License-Identifier: LPPL-1.0+ OR BSD-2-Clause
+
+%% This file is used for including the LaTeX ontology mappings. 

document-generator/document-template/root-cenelec_50126-scrreprt.tex

@@ -1,74 +0,0 @@
-%% Copyright (C) 2018 The University of Sheffield
-%%               2018 The University of Paris-Sud
-%%
-%% 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 of the License, or any later version.
-%%   OR
-%%   The 2-clause BSD-style license.
-%%  
-%%   SPDX-License-Identifier: LPPL-1
-
-%% Warning: Do Not Edit!
-%% =====================
-%% This is the root file for the Isabelle/DOF. 
-%% All customization and/or additional packages should be added to the file 
-%% preamble.tex. 
-
-
-\RequirePackage{ifvtex}
-\documentclass[fontsize=10pt,DIV12,paper=a4,open=right,twoside,abstract=true]{scrreprt}
-\usepackage[T1]{fontenc}
-\usepackage[utf8]{inputenc}
-\usepackage{textcomp}
-\usepackage[english]{babel}
-\usepackage{isabelle}
-\usepackage{DOF-cenelec_50126}
-\usepackage{isabellesym}
-\usepackage{amsmath}
-\usepackage{amssymb}
-\usepackage[numbers, sort&compress, sectionbib]{natbib}
-\usepackage{hyperref}
-\setcounter{tocdepth}{3} 
-\hypersetup{%
-   bookmarksdepth=3
-  ,pdfpagelabels
-  ,pageanchor=false
-  ,bookmarksnumbered
-  ,plainpages=false
-} % more detailed digital TOC (aka bookmarks)
-\sloppy
-\allowdisplaybreaks[4]
-\urlstyle{rm}
-\isabellestyle{it}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%%% Overrides the (rightfully issued) warning by Koma Script that \rm
-%%% etc. should not be used (they are deprecated since more than a
-%%% decade)
-  \DeclareOldFontCommand{\rm}{\normalfont\rmfamily}{\mathrm}
-  \DeclareOldFontCommand{\sf}{\normalfont\sffamily}{\mathsf}
-  \DeclareOldFontCommand{\tt}{\normalfont\ttfamily}{\mathtt}
-  \DeclareOldFontCommand{\bf}{\normalfont\bfseries}{\mathbf}
-  \DeclareOldFontCommand{\it}{\normalfont\itshape}{\mathit}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-
-\title{<TITLE>}
-\author{<AUTHOR>}
-\begin{document}
-\maketitle
-\tableofcontents
-\input{session}
-% optional bibliography
-\IfFileExists{root.bib}{%
-    \bibliographystyle{abbrvnat}
-    \bibliography{root}
-}{}
-\end{document}
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: t
-%%% End:

document-generator/document-template/root-lncs.tex

@@ -13,7 +13,7 @@
 
 %% Warning: Do Not Edit!
 %% =====================
-%% This is the root file for the Isabelle/DOF configuration "scholarly_paper/lncs". 
+%% This is the root file for the Isabelle/DOF using Springer's llncs.cls.
 %% All customization and/or additional packages should be added to the file 
 %% preamble.tex. 
 
@@ -28,7 +28,7 @@
 \usepackage{amsmath}
 \usepackage{amssymb}
 \usepackage[numbers, sort&compress, sectionbib]{natbib}
-\usepackage{DOF-scholarly_paper-lncs}
+\input{ontologies}
 \IfFileExists{preamble.tex}{\input{preamble.tex}}{}%
 \usepackage{xspace}
 \newcommand{\isadof}{Isabelle/DOF\xspace}

document-generator/document-template/root-scrreprt.tex

@@ -25,7 +25,7 @@
 \usepackage{textcomp}
 \usepackage[english]{babel}
 \usepackage{isabelle}
-\usepackage{DOF}
+\input{ontologies}
 \usepackage{isabellesym}
 \usepackage{amsmath}
 \usepackage{amssymb}

document-generator/latex/DOF-cenelec_50126.sty

@@ -16,7 +16,7 @@
   [0000/00/00 Unreleased v0.0.0+%
   Document-Type Support Framework for Isabelle (CENELEC 50126).]
 
-\RequirePackage{DOF}
+\RequirePackage{DOF-core}
 
 
 \newkeycommand\isaDofSectionRequirement[label=,type=,main_author=,long_name=][1]{%

document-generator/latex/DOF-core.sty

@@ -12,7 +12,7 @@
 %%   SPDX-License-Identifier: LPPL-1.0+ OR BSD-2-Clause
 
 \NeedsTeXFormat{LaTeX2e}\relax
-\ProvidesPackage{DOF}
+\ProvidesPackage{DOF-core}
   [0000/00/00 Unreleased v0.0.0+%
   Document-Type Support Framework for Isabelle.]
 

document-generator/latex/DOF-scholarly_paper.sty

@@ -16,7 +16,7 @@
   [0000/00/00 Unreleased v0.0.0+%
   Document-Type Support Framework for Isabelle (LNCS).]
 
-\RequirePackage{DOF}
+\RequirePackage{DOF-core}
 
 
 \newkeycommand\isaDofSectionIntroduction[label=,type=,main_author=,fixme_list=][1]{%