Merge branch 'main' into isabelle_nightly

.woodpecker/mk_release

@@ -93,11 +93,11 @@ build_and_install_manuals()
         else
             echo "  * Quick and Dirty Mode (running on CI)"
             mkdir -p $ISADOF_WORK_DIR/Isabelle_DOF-Example-I/output/
-            cp $ARTIFACT_DIR/browser_info/Unsorted/Isabelle_DOF-Example-I/document.pdf \
+            cp $ARTIFACT_DIR/browser_info/AFP/Isabelle_DOF-Example-I/document.pdf \
                $ISADOF_WORK_DIR/Isabelle_DOF-Example-I/output/
  
             mkdir -p $ISADOF_WORK_DIR/Isabelle_DOF/output/
-            cp $ARTIFACT_DIR/browser_info/Unsorted/Isabelle_DOF/document.pdf \
+            cp $ARTIFACT_DIR/browser_info/AFP/Isabelle_DOF/document.pdf \
                $ISADOF_WORK_DIR/Isabelle_DOF/output/;
         fi
     else

Isabelle_DOF-Examples-Extra/ROOTS

@@ -2,3 +2,4 @@ technical_report
 CENELEC_50128
 cytology
 CC_ISO15408
+beamerx

Isabelle_DOF-Examples-Extra/beamerx/ROOTS

@@ -0,0 +1,2 @@
+poster
+presentation

Isabelle_DOF-Examples-Extra/beamerx/poster/ROOT

@@ -0,0 +1,8 @@
+chapter AFP 
+
+session "poster-example" (AFP) = "Isabelle_DOF-Ontologies" +
+  options [document = pdf, document_output = "output", document_build = dof, timeout = 300]
+  theories
+    "poster"
+  document_files
+    "preamble.tex"

Isabelle_DOF-Examples-Extra/beamerx/poster/document/preamble.tex

@@ -0,0 +1,2 @@
+%% This is a placeholder for user-specific configuration and packages.
+

Isabelle_DOF-Examples-Extra/beamerx/poster/poster.thy

@@ -0,0 +1,35 @@
+(*<*)
+theory "poster"
+  imports "Isabelle_DOF.scholarly_paper"
+ "Isabelle_DOF-Ontologies.document_templates"
+begin
+
+use_template "beamerposter-UNSUPPORTED"
+use_ontology "scholarly_paper"
+(*>*)
+
+title*[tit::title]\<open>Example Presentation\<close>
+                                  
+author*[safouan,email="\<open>example@example.org\<close>",affiliation="\<open>Example Org\<close>"]\<open>Eliza Example\<close>
+
+text\<open>
+    \vfill
+    \begin{block}{\large Fontsizes}
+      \centering
+      {\tiny tiny}\par
+      {\scriptsize scriptsize}\par
+      {\footnotesize footnotesize}\par
+      {\normalsize normalsize}\par
+      {\large large}\par
+      {\Large Large}\par
+      {\LARGE LARGE}\par
+      {\veryHuge veryHuge}\par
+      {\VeryHuge VeryHuge}\par
+      {\VERYHuge VERYHuge}\par
+    \end{block}
+    \vfill
+\<close>
+
+(*<*)
+end 
+(*>*)

Isabelle_DOF-Examples-Extra/beamerx/presentation/ROOT

@@ -0,0 +1,8 @@
+chapter AFP 
+
+session "presentation-example" (AFP) = "Isabelle_DOF-Ontologies" +
+  options [document = pdf, document_output = "output", document_build = dof, timeout = 300]
+  theories
+    "presentation"
+  document_files
+    "preamble.tex"

Isabelle_DOF-Examples-Extra/beamerx/presentation/document/preamble.tex

@@ -0,0 +1,2 @@
+%% This is a placeholder for user-specific configuration and packages.
+

Isabelle_DOF-Examples-Extra/beamerx/presentation/presentation.thy

@@ -0,0 +1,24 @@
+(*<*)
+theory "presentation"
+  imports "Isabelle_DOF.scholarly_paper"
+ "Isabelle_DOF-Ontologies.document_templates"
+begin
+
+use_template "beamer-UNSUPPORTED"
+use_ontology "scholarly_paper"
+(*>*)
+
+title*[tit::title]\<open>Example Presentation\<close>
+                                  
+author*[safouan,email="\<open>example@example.org\<close>",affiliation="\<open>Example Org\<close>"]\<open>Eliza Example\<close>
+
+text\<open>
+\begin{frame}
+\frametitle{Example Slide}
+\centering\huge This is an example!
+\end{frame}
+\<close>
+
+(*<*)
+end 
+(*>*)

Isabelle_DOF-Ontologies/CENELEC_50128/DOF-CENELEC_50128.sty

@@ -60,26 +60,26 @@
 }
 
 \newcommand{\SRACautorefname}{SRAC}
-\newisadof{textDOTCENELECUNDERSCORE50128DOTSRAC}%
+\newisadof{textDOTCENELECUNDERSCOREFIVEZEROONETWOEIGHTDOTSRAC}%
 [label=,type=%
 ,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel=%
 ,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable=%
 ,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants=%
-,CENELECUNDERSCORE50128DOTrequirementDOTisUNDERSCOREconcerned=%
+,CENELECUNDERSCOREFIVEZEROONETWOEIGHTDOTrequirementDOTisUNDERSCOREconcerned=%
-,CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname=%
+,CENELECUNDERSCOREFIVEZEROONETWOEIGHTDOTrequirementDOTlongUNDERSCOREname=%
-,CENELECUNDERSCORE50128DOTSRACDOTformalUNDERSCORErepr=%
+,CENELECUNDERSCOREFIVEZEROONETWOEIGHTDOTSRACDOTformalUNDERSCORErepr=%
-,CENELECUNDERSCORE50128DOTSRACDOTassumptionUNDERSCOREkind=%
+,CENELECUNDERSCOREFIVEZEROONETWOEIGHTDOTSRACDOTassumptionUNDERSCOREkind=%
-,CENELECUNDERSCORE50128DOTECDOTassumptionUNDERSCOREkind=%
+,CENELECUNDERSCOREFIVEZEROONETWOEIGHTDOTECDOTassumptionUNDERSCOREkind=%
-,CENELECUNDERSCORE50128DOTassumptionDOTassumptionUNDERSCOREkind=%
+,CENELECUNDERSCOREFIVEZEROONETWOEIGHTDOTassumptionDOTassumptionUNDERSCOREkind=%
 ][1]{%
   \begin{isamarkuptext}%
-      \ifthenelse{\equal{\commandkey{CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname}}{}}{%
+      \ifthenelse{\equal{\commandkey{CENELECUNDERSCOREFIVEZEROONETWOEIGHTDOTrequirementDOTlongUNDERSCOREname}}{}}{%
         \begin{SRAC}%
             \addxcontentsline{tos}{chapter}[]{\autoref{\commandkey{label}}}%
       }{%
-        \begin{SRAC}[\commandkey{CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname}]%
+        \begin{SRAC}[\commandkey{CENELECUNDERSCOREFIVEZEROONETWOEIGHTDOTrequirementDOTlongUNDERSCOREname}]%
-          \addxcontentsline{tos}{chapter}[]{\autoref{\commandkey{label}}: \commandkey{CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname}}%
+          \addxcontentsline{tos}{chapter}[]{\autoref{\commandkey{label}}: \commandkey{CENELECUNDERSCOREFIVEZEROONETWOEIGHTDOTrequirementDOTlongUNDERSCOREname}}%
-          \DOFindex{SRAC}{\commandkey{CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname}}%
+          \DOFindex{SRAC}{\commandkey{CENELECUNDERSCOREFIVEZEROONETWOEIGHTDOTrequirementDOTlongUNDERSCOREname}}%
       }\label{\commandkey{label}}%
       #1%
     \end{SRAC}
@@ -113,26 +113,26 @@
 }
 
 \newcommand{\ECautorefname}{EC}
-\newisadof{textDOTCENELECUNDERSCORE50128DOTEC}%
+\newisadof{textDOTCENELECUNDERSCOREFIVEZEROONETWOEIGHTDOTEC}%
 [label=,type=%
 ,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel=%
 ,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable=%
 ,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants=%
-,CENELECUNDERSCORE50128DOTrequirementDOTisUNDERSCOREconcerned=%
+,CENELECUNDERSCOREFIVEZEROONETWOEIGHTDOTrequirementDOTisUNDERSCOREconcerned=%
-,CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname=%
+,CENELECUNDERSCOREFIVEZEROONETWOEIGHTDOTrequirementDOTlongUNDERSCOREname=%
-,CENELECUNDERSCORE50128DOTSRACDOTformalUNDERSCORErepr=%
+,CENELECUNDERSCOREFIVEZEROONETWOEIGHTDOTSRACDOTformalUNDERSCORErepr=%
-,CENELECUNDERSCORE50128DOTSRACDOTassumptionUNDERSCOREkind=%
+,CENELECUNDERSCOREFIVEZEROONETWOEIGHTDOTSRACDOTassumptionUNDERSCOREkind=%
-,CENELECUNDERSCORE50128DOTECDOTassumptionUNDERSCOREkind=%
+,CENELECUNDERSCOREFIVEZEROONETWOEIGHTDOTECDOTassumptionUNDERSCOREkind=%
-,CENELECUNDERSCORE50128DOTassumptionDOTassumptionUNDERSCOREkind=%
+,CENELECUNDERSCOREFIVEZEROONETWOEIGHTDOTassumptionDOTassumptionUNDERSCOREkind=%
 ][1]{%
   \begin{isamarkuptext}%
-      \ifthenelse{\equal{\commandkey{CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname}}{}}{%
+      \ifthenelse{\equal{\commandkey{CENELECUNDERSCOREFIVEZEROONETWOEIGHTDOTrequirementDOTlongUNDERSCOREname}}{}}{%
         \begin{EC}%
             \addxcontentsline{tos}{chapter}[]{\autoref{\commandkey{label}}}%
       }{%
-        \begin{EC}[\commandkey{CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname}]%
+        \begin{EC}[\commandkey{CENELECUNDERSCOREFIVEZEROONETWOEIGHTDOTrequirementDOTlongUNDERSCOREname}]%
-          \addxcontentsline{toe}{chapter}[]{\autoref{\commandkey{label}}: \commandkey{CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname}}%
+          \addxcontentsline{toe}{chapter}[]{\autoref{\commandkey{label}}: \commandkey{CENELECUNDERSCOREFIVEZEROONETWOEIGHTDOTrequirementDOTlongUNDERSCOREname}}%
-          \DOFindex{EC}{\commandkey{CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname}}%
+          \DOFindex{EC}{\commandkey{CENELECUNDERSCOREFIVEZEROONETWOEIGHTDOTrequirementDOTlongUNDERSCOREname}}%
       }\label{\commandkey{label}}%
       #1%
     \end{EC}
@@ -155,23 +155,23 @@
 }
 
 \newcommand{\assumptionautorefname}{assumption}
-\newisadof{textDOTCENELECUNDERSCORE50128DOTassumption}%
+\newisadof{textDOTCENELECUNDERSCOREFIVEZEROONETWOEIGHTDOTassumption}%
 [label=,type=%
 ,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel=%
 ,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable=%
 ,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants=%
-,CENELECUNDERSCORE50128DOTrequirementDOTisUNDERSCOREconcerned=%
+,CENELECUNDERSCOREFIVEZEROONETWOEIGHTDOTrequirementDOTisUNDERSCOREconcerned=%
-,CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname=%
+,CENELECUNDERSCOREFIVEZEROONETWOEIGHTDOTrequirementDOTlongUNDERSCOREname=%
-,CENELECUNDERSCORE50128DOTSRACDOTformalUNDERSCORErepr=%
+,CENELECUNDERSCOREFIVEZEROONETWOEIGHTDOTSRACDOTformalUNDERSCORErepr=%
-,CENELECUNDERSCORE50128DOTSRACDOTassumptionUNDERSCOREkind=%
+,CENELECUNDERSCOREFIVEZEROONETWOEIGHTDOTSRACDOTassumptionUNDERSCOREkind=%
-,CENELECUNDERSCORE50128DOTassumptionDOTassumptionUNDERSCOREkind=%
+,CENELECUNDERSCOREFIVEZEROONETWOEIGHTDOTassumptionDOTassumptionUNDERSCOREkind=%
 ][1]{%
   \begin{isamarkuptext}%
-      \ifthenelse{\equal{\commandkey{CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname}}{}}{%
+      \ifthenelse{\equal{\commandkey{CENELECUNDERSCOREFIVEZEROONETWOEIGHTDOTrequirementDOTlongUNDERSCOREname}}{}}{%
         \begin{assumption}%
       }{%
-        \begin{assumption}[\commandkey{CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname}]%
+        \begin{assumption}[\commandkey{CENELECUNDERSCOREFIVEZEROONETWOEIGHTDOTrequirementDOTlongUNDERSCOREname}]%
-          \DOFindex{assumption}{\commandkey{CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname}}%
+          \DOFindex{assumption}{\commandkey{CENELECUNDERSCOREFIVEZEROONETWOEIGHTDOTrequirementDOTlongUNDERSCOREname}}%
       }\label{\commandkey{label}}%
       #1%
     \end{assumption}
@@ -196,23 +196,23 @@
 
 
 \newcommand{\hypothesisautorefname}{hypothesis}
-\newisadof{textDOTCENELECUNDERSCORE50128DOThypothesis}%
+\newisadof{textDOTCENELECUNDERSCOREFIVEZEROONETWOEIGHTDOThypothesis}%
 [label=,type=%
 ,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTlevel=%
 ,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTreferentiable=%
 ,IsaUNDERSCORECOLDOTtextUNDERSCOREelementDOTvariants=%
-,CENELECUNDERSCORE50128DOTrequirementDOTisUNDERSCOREconcerned=%
+,CENELECUNDERSCOREFIVEZEROONETWOEIGHTDOTrequirementDOTisUNDERSCOREconcerned=%
-,CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname=%
+,CENELECUNDERSCOREFIVEZEROONETWOEIGHTDOTrequirementDOTlongUNDERSCOREname=%
-,CENELECUNDERSCORE50128DOTSRACDOTformalUNDERSCORErepr=%
+,CENELECUNDERSCOREFIVEZEROONETWOEIGHTDOTSRACDOTformalUNDERSCORErepr=%
-,CENELECUNDERSCORE50128DOTSRACDOThypothesisUNDERSCOREkind=%
+,CENELECUNDERSCOREFIVEZEROONETWOEIGHTDOTSRACDOThypothesisUNDERSCOREkind=%
-,CENELECUNDERSCORE50128DOThypothesisDOThypUNDERSCOREtype=%
+,CENELECUNDERSCOREFIVEZEROONETWOEIGHTDOThypothesisDOThypUNDERSCOREtype=%
 ][1]{%
   \begin{isamarkuptext}%
-      \ifthenelse{\equal{\commandkey{CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname}}{}}{%
+      \ifthenelse{\equal{\commandkey{CENELECUNDERSCOREFIVEZEROONETWOEIGHTDOTrequirementDOTlongUNDERSCOREname}}{}}{%
         \begin{hypothesis}%
       }{%
-        \begin{hypothesis}[\commandkey{CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname}]%
+        \begin{hypothesis}[\commandkey{CENELECUNDERSCOREFIVEZEROONETWOEIGHTDOTrequirementDOTlongUNDERSCOREname}]%
-          \DOFindex{hypothesis}{\commandkey{CENELECUNDERSCORE50128DOTrequirementDOTlongUNDERSCOREname}}%
+          \DOFindex{hypothesis}{\commandkey{CENELECUNDERSCOREFIVEZEROONETWOEIGHTDOTrequirementDOTlongUNDERSCOREname}}%
       }\label{\commandkey{label}}%
       #1%
     \end{hypothesis}

Isabelle_DOF-Ontologies/document-templates/root-beamer-UNSUPPORTED.tex

@@ -0,0 +1,64 @@
+%% Copyright (c) University of Exeter
+%%               University of Paris-Saclay
+%%
+%% 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
+
+%% Warning: Do Not Edit!
+%% =====================
+%% This is the root file for the Isabelle/DOF using the scrartcl class.
+%%
+%% All customization and/or additional packages should be added to the file
+%% preamble.tex.
+
+\RequirePackage{ifvtex}
+\documentclass[16x9,9pt]{beamer}
+\PassOptionsToPackage{force}{DOF-scholarly_paper}
+\usepackage{DOF-core}
+
+\usepackage{textcomp}
+\bibliographystyle{abbrvnat}
+\RequirePackage{subcaption}
+
+\providecommand{\institute}[1]{}%
+\providecommand{\inst}[1]{}%
+\providecommand{\orcidID}[1]{}%
+\providecommand{\email}[1]{}%
+
+
+\usepackage[numbers, sort&compress, sectionbib]{natbib}
+
+\usepackage{hyperref}
+\setcounter{tocdepth}{3} 
+\hypersetup{%
+   bookmarksdepth=3
+  ,pdfpagelabels
+  ,pageanchor=true
+  ,bookmarksnumbered
+  ,plainpages=false
+} % more detailed digital TOC (aka bookmarks)
+\sloppy
+\allowdisplaybreaks[4]
+
+\newenvironment{frontmatter}{}{}
+\raggedbottom
+\begin{document}
+\begin{frame}
+  \maketitle
+\end{frame}
+\IfFileExists{dof_session.tex}{\input{dof_session}}{\input{session}}
+% optional bibliography
+\IfFileExists{root.bib}{{\bibliography{root}}}{}
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:

Isabelle_DOF-Ontologies/document-templates/root-beamerposter-UNSUPPORTED.tex

@@ -0,0 +1,64 @@
+%% Copyright (c) University of Exeter
+%%               University of Paris-Saclay
+%%
+%% 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
+
+%% Warning: Do Not Edit!
+%% =====================
+%% This is the root file for the Isabelle/DOF using the scrartcl class.
+%%
+%% All customization and/or additional packages should be added to the file
+%% preamble.tex.
+
+\RequirePackage{ifvtex}
+\documentclass[]{beamer}
+\PassOptionsToPackage{force}{DOF-scholarly_paper}
+\usepackage{beamerposter}
+\usepackage{DOF-core}
+
+\usepackage{textcomp}
+\bibliographystyle{abbrvnat}
+\RequirePackage{subcaption}
+
+\providecommand{\institute}[1]{}%
+\providecommand{\inst}[1]{}%
+\providecommand{\orcidID}[1]{}%
+\providecommand{\email}[1]{}%
+
+
+\usepackage[numbers, sort&compress, sectionbib]{natbib}
+
+\usepackage{hyperref}
+\setcounter{tocdepth}{3} 
+\hypersetup{%
+   bookmarksdepth=3
+  ,pdfpagelabels
+  ,pageanchor=true
+  ,bookmarksnumbered
+  ,plainpages=false
+} % more detailed digital TOC (aka bookmarks)
+\sloppy
+\allowdisplaybreaks[4]
+
+\newenvironment{frontmatter}{}{}
+\raggedbottom
+\begin{document}
+\begin{frame}[fragile]
+\IfFileExists{dof_session.tex}{\input{dof_session}}{\input{session}}
+% optional bibliography
+\IfFileExists{root.bib}{{\bibliography{root}}}{}
+\end{frame}
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:

Isabelle_DOF-Ontologies/document_templates.thy

@@ -25,4 +25,8 @@ define_template "./document-templates/root-svjour3-UNSUPPORTED.tex"
                 "Unsupported template for SVJOUR. Not for general use."
 define_template "./document-templates/root-sn-article-UNSUPPORTED.tex" 
                 "Unsupported template for Springer Nature's template. Not for general use."
+define_template "./document-templates/root-beamer-UNSUPPORTED.tex" 
+                "Unsupported template for presentations. Not for general use."
+define_template "./document-templates/root-beamerposter-UNSUPPORTED.tex" 
+                "Unsupported template for poster. Not for general use."
 end