diff --git a/document-generator/Tools/DOF_mkroot b/document-generator/Tools/DOF_mkroot index b48ab2e3..63a711f9 100755 --- a/document-generator/Tools/DOF_mkroot +++ b/document-generator/Tools/DOF_mkroot @@ -135,17 +135,15 @@ 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 - sed -i -e "s/root.tex/root.inf/" "$DIR"/ROOT + sed -i -e "s/root.tex/isadof.cfg/" "$DIR"/ROOT rm -f "$DIR"/document/root.tex TITLE=$(echo "$NAME" | tr _ - | tr -d '\\') AUTHOR=$(echo "By $USER" | tr _ - | tr -d '\\') - echo $TEMPLATE > "$DIR"/document/root.inf + echo "Template: $TEMPLATE" > "$DIR"/document/isadof.cfg cp "$ISABELLE_HOME_USER/DOF/document-template/build" "$DIR"/document/ - cp "$ISABELLE_HOME_USER/DOF/document-template/ontologies.tex" "$DIR"/document/ for o in $ONTOLOGY; do - echo "\usepackage{DOF-$o}" >> "$DIR"/document/ontologies.tex; + echo "Ontology: $o" >> "$DIR"/document/isadof.cfg; done sed -e "s//$AUTHOR/" -e "s//$TITLE/" "$ISABELLE_HOME_USER/DOF/document-template/preamble.tex" > "$DIR"/document/preamble.tex else diff --git a/document-generator/document-template/build_lib.sh b/document-generator/document-template/build_lib.sh index 8aa2a9b9..6de6fcf6 100755 --- a/document-generator/document-template/build_lib.sh +++ b/document-generator/document-template/build_lib.sh @@ -49,17 +49,64 @@ if [ ! -f $ISABELLE_HOME_USER/DOF/latex/DOF-core.sty ]; then exit 1 fi -if [ ! -f root.inf ]; then +if [ -f "$DIR/$ROOT_NAME.tex" ]; then + echo "" + echo "Error: Found root file ($DIR/$ROOT_NAME.tex)" + echo "=====" + echo "Isabelle/DOF does not use the Isabelle root file setup. Please check" + echo "your project setup. Your $DIR/isadof.cfg should define a Isabelle/DOF" + echo "template and your project should not include a root file." + echo "" + exit 1 +fi + +if [ -f "$DIR/ontologies.tex" ]; then + echo "" + echo "Error: Old project setup, found a ontologies file ($DIR/ontologies.tex)" + echo "=====" + echo "Isabelle/DOF does no longer support the use of $DIR/ontologies.tex. The" + echo "required ontologies should be defined in $DIR/isadof.cfg." + echo "" + exit 1 +fi + +if [ -f "$DIR/$ROOT_NAME.tex" ]; then + echo "" + echo "Error: Found root file ($DIR/$ROOT_NAME.tex)" + echo "=====" + echo "Isabelle/DOF does not make use of the Isabelle root file mechanism." + echo "Please check your Isabelle/DOF setup." + exit 1 +fi + +if [ ! -f isadof.cfg ]; then echo "" echo "Error: Isabelle/DOF document setup not correct" echo "=====" - echo "Could not find root.inf. Please upgrade your Isabelle/DOF document" + echo "Could not find isadof.cfg. Please upgrade your Isabelle/DOF document" echo "setup manually." exit 1 fi -ROOT="$ISABELLE_HOME_USER/DOF/document-template/root-$(cat root.inf).tex" -if [ ! -f $ROOT]; then +TEMPLATE="" +ONTOLOGY="core" +CONFIG="isadof.cfg" +while IFS= read -r line;do + fields=($(printf "%s" "$line"|cut -d':' --output-delimiter=' ' -f1-)) + if [[ "${fields[0]}" = "Template" ]]; then + TEMPLATE="${fields[1]}" + fi + if [[ "${fields[0]}" = "Ontology" ]]; then + ONTOLOGY="$ONTOLOGY ${fields[1]}" + fi +done < $CONFIG + +for o in $ONTOLOGY; do + echo "\usepackage{DOF-$o}" >> ontologies.tex; +done + +ROOT="$ISABELLE_HOME_USER/DOF/document-template/root-$TEMPLATE.tex" +if [ ! -f $ROOT ]; then echo "" echo "Error: Isabelle/DOF document setup not correct" echo "=====" @@ -72,10 +119,10 @@ cp $ROOT root.tex cp $ISABELLE_HOME_USER/DOF/latex/*.sty . cp $ISABELLE_HOME_USER/DOF/latex/*.sty . -$ISABELLE_TOOL latex -o sty "$ROOT_NAME.tex" && \ -$ISABELLE_TOOL latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \ -{ [ ! -f "$ROOT_NAME.bib" ] || $ISABELLE_TOOL latex -o bbl "$ROOT_NAME.tex"; } && \ -{ [ ! -f "$ROOT_NAME.idx" ] || $ISABELLE_TOOL latex -o idx "$ROOT_NAME.tex"; } && \ -$ISABELLE_TOOL latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \ -$ISABELLE_TOOL latex -o "$OUTFORMAT" "$ROOT_NAME.tex" +$ISABELLE_TOOL latex -o sty "root.tex" && \ +$ISABELLE_TOOL latex -o "$OUTFORMAT" "root.tex" && \ +{ [ ! -f "$ROOT_NAME.bib" ] || $ISABELLE_TOOL latex -o bbl "root.tex"; } && \ +{ [ ! -f "$ROOT_NAME.idx" ] || $ISABELLE_TOOL latex -o idx "root.tex"; } && \ +$ISABELLE_TOOL latex -o "$OUTFORMAT" "root.tex" && \ +$ISABELLE_TOOL latex -o "$OUTFORMAT" "root.tex" diff --git a/document-generator/document-template/ontologies.tex b/document-generator/document-template/ontologies.tex deleted file mode 100644 index 88f585f8..00000000 --- a/document-generator/document-template/ontologies.tex +++ /dev/null @@ -1,14 +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.0+ OR BSD-2-Clause - -%% This file is used for including the LaTeX ontology mappings. diff --git a/examples/math_exam/BAC2017/ROOT b/examples/math_exam/BAC2017/ROOT index 61540428..cf671977 100644 --- a/examples/math_exam/BAC2017/ROOT +++ b/examples/math_exam/BAC2017/ROOT @@ -6,7 +6,6 @@ session "BAC2017" = "Isabelle_DOF" + theories BAC2017 document_files - "root.inf" + "isadof.cfg" "preamble.tex" - "ontologies.tex" "build" diff --git a/examples/math_exam/BAC2017/document/isadof.cfg b/examples/math_exam/BAC2017/document/isadof.cfg new file mode 100644 index 00000000..f13f22b5 --- /dev/null +++ b/examples/math_exam/BAC2017/document/isadof.cfg @@ -0,0 +1,2 @@ +Template: scrartcl +Ontology: mathex diff --git a/examples/math_exam/BAC2017/document/ontologies.tex b/examples/math_exam/BAC2017/document/ontologies.tex deleted file mode 100644 index 8e80a84c..00000000 --- a/examples/math_exam/BAC2017/document/ontologies.tex +++ /dev/null @@ -1,17 +0,0 @@ -% This file was modified by the DOF LaTeX converter, version 0.0.3 -%% 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. -\usepackage{DOF-core} -\usepackage{DOF-mathex} diff --git a/examples/math_exam/BAC2017/document/root.inf b/examples/math_exam/BAC2017/document/root.inf deleted file mode 100644 index 52343f0f..00000000 --- a/examples/math_exam/BAC2017/document/root.inf +++ /dev/null @@ -1 +0,0 @@ -scrartcl diff --git a/examples/math_exam/MathExam/ROOT b/examples/math_exam/MathExam/ROOT index 3474ce43..9f5e87ee 100644 --- a/examples/math_exam/MathExam/ROOT +++ b/examples/math_exam/MathExam/ROOT @@ -4,8 +4,7 @@ session "MathExam" = "Isabelle_DOF" + MathExam document_files "preamble.tex" - "root.inf" - "ontologies.tex" + "isadof.cfg" "preamble.tex" "build" "figures/Polynomialdeg5.png" diff --git a/examples/math_exam/MathExam/document/isadof.cfg b/examples/math_exam/MathExam/document/isadof.cfg new file mode 100644 index 00000000..f13f22b5 --- /dev/null +++ b/examples/math_exam/MathExam/document/isadof.cfg @@ -0,0 +1,2 @@ +Template: scrartcl +Ontology: mathex diff --git a/examples/math_exam/MathExam/document/ontologies.tex b/examples/math_exam/MathExam/document/ontologies.tex deleted file mode 100644 index 8e80a84c..00000000 --- a/examples/math_exam/MathExam/document/ontologies.tex +++ /dev/null @@ -1,17 +0,0 @@ -% This file was modified by the DOF LaTeX converter, version 0.0.3 -%% 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. -\usepackage{DOF-core} -\usepackage{DOF-mathex} diff --git a/examples/math_exam/MathExam/document/root.inf b/examples/math_exam/MathExam/document/root.inf deleted file mode 100644 index 52343f0f..00000000 --- a/examples/math_exam/MathExam/document/root.inf +++ /dev/null @@ -1 +0,0 @@ -scrartcl diff --git a/examples/scholarly_paper/2018_cicm/ROOT b/examples/scholarly_paper/2018_cicm/ROOT index fac0be9a..0ea790b9 100644 --- a/examples/scholarly_paper/2018_cicm/ROOT +++ b/examples/scholarly_paper/2018_cicm/ROOT @@ -3,12 +3,11 @@ session "IsaDofApplications" = "Isabelle_DOF" + theories IsaDofApplications document_files - "root.inf" + "isadof.cfg" "root.bib" "preamble.tex" "build" "lstisadof.sty" - "ontologies.tex" "figures/isabelle-architecture.pdf" "figures/Dogfood-Intro.png" "figures/InteractiveMathSheet.png" diff --git a/examples/scholarly_paper/2018_cicm/document/isadof.cfg b/examples/scholarly_paper/2018_cicm/document/isadof.cfg new file mode 100644 index 00000000..dbf4a8e6 --- /dev/null +++ b/examples/scholarly_paper/2018_cicm/document/isadof.cfg @@ -0,0 +1,2 @@ +Template: scrartcl +Ontology: scholarly_paper diff --git a/examples/scholarly_paper/2018_cicm/document/ontologies.tex b/examples/scholarly_paper/2018_cicm/document/ontologies.tex deleted file mode 100644 index 33e9548e..00000000 --- a/examples/scholarly_paper/2018_cicm/document/ontologies.tex +++ /dev/null @@ -1,17 +0,0 @@ -% This file was modified by the DOF LaTeX converter, version 0.0.3 -%% 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. -\usepackage{DOF-core} -\usepackage{DOF-scholarly_paper} \ No newline at end of file diff --git a/examples/scholarly_paper/2018_cicm/document/root.inf b/examples/scholarly_paper/2018_cicm/document/root.inf deleted file mode 100644 index 52343f0f..00000000 --- a/examples/scholarly_paper/2018_cicm/document/root.inf +++ /dev/null @@ -1 +0,0 @@ -scrartcl diff --git a/examples/technical_report/IsaDof_Manual/ROOT b/examples/technical_report/IsaDof_Manual/ROOT index 1a0b5fd8..fbbd4391 100644 --- a/examples/technical_report/IsaDof_Manual/ROOT +++ b/examples/technical_report/IsaDof_Manual/ROOT @@ -3,12 +3,11 @@ session "IsaDof_Manual" = "Isabelle_DOF" + theories IsaDofManual document_files - "root.inf" + "isadof.cfg" "root.bib" "preamble.tex" "build" "lstisadof.sty" - "ontologies.tex" "figures/isabelle-architecture.pdf" "figures/Dogfood-Intro.png" "figures/InteractiveMathSheet.png" diff --git a/examples/technical_report/IsaDof_Manual/document/isadof.cfg b/examples/technical_report/IsaDof_Manual/document/isadof.cfg new file mode 100644 index 00000000..849fad5e --- /dev/null +++ b/examples/technical_report/IsaDof_Manual/document/isadof.cfg @@ -0,0 +1,2 @@ +Template: scrreprt +Ontology: technical_report diff --git a/examples/technical_report/IsaDof_Manual/document/ontologies.tex b/examples/technical_report/IsaDof_Manual/document/ontologies.tex deleted file mode 100644 index 47fcfd6c..00000000 --- a/examples/technical_report/IsaDof_Manual/document/ontologies.tex +++ /dev/null @@ -1,16 +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.0+ OR BSD-2-Clause - -%% This file is used for including the LaTeX ontology mappings. -\usepackage{DOF-core} -\usepackage{DOF-technical_report} diff --git a/examples/technical_report/IsaDof_Manual/document/root.inf b/examples/technical_report/IsaDof_Manual/document/root.inf deleted file mode 100644 index 234a54b2..00000000 --- a/examples/technical_report/IsaDof_Manual/document/root.inf +++ /dev/null @@ -1 +0,0 @@ -scrreprt diff --git a/examples/technical_report/TR_my_commented_isabelle/ROOT b/examples/technical_report/TR_my_commented_isabelle/ROOT index e992146a..ce596f76 100644 --- a/examples/technical_report/TR_my_commented_isabelle/ROOT +++ b/examples/technical_report/TR_my_commented_isabelle/ROOT @@ -3,9 +3,8 @@ session "TR_mycommentedisabelle" = "Isabelle_DOF" + theories "MyCommentedIsabelle" document_files - "root.inf" + "isadof.cfg" "preamble.tex" - "ontologies.tex" "prooftree.sty" "build" "figures/text-element.pdf" diff --git a/examples/technical_report/TR_my_commented_isabelle/document/isadof.cfg b/examples/technical_report/TR_my_commented_isabelle/document/isadof.cfg new file mode 100644 index 00000000..849fad5e --- /dev/null +++ b/examples/technical_report/TR_my_commented_isabelle/document/isadof.cfg @@ -0,0 +1,2 @@ +Template: scrreprt +Ontology: technical_report diff --git a/examples/technical_report/TR_my_commented_isabelle/document/ontologies.tex b/examples/technical_report/TR_my_commented_isabelle/document/ontologies.tex deleted file mode 100644 index 47fcfd6c..00000000 --- a/examples/technical_report/TR_my_commented_isabelle/document/ontologies.tex +++ /dev/null @@ -1,16 +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.0+ OR BSD-2-Clause - -%% This file is used for including the LaTeX ontology mappings. -\usepackage{DOF-core} -\usepackage{DOF-technical_report} diff --git a/examples/technical_report/TR_my_commented_isabelle/document/root.inf b/examples/technical_report/TR_my_commented_isabelle/document/root.inf deleted file mode 100644 index 234a54b2..00000000 --- a/examples/technical_report/TR_my_commented_isabelle/document/root.inf +++ /dev/null @@ -1 +0,0 @@ -scrreprt