Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Further updates to the new project structure (contributes to #23).
ci/woodpecker/push/build Pipeline was successful Details

This commit is contained in:
Achim D. Brucker 2023-02-28 05:20:01 +00:00
parent 10b4eaf660
commit 058324ab5d
2 changed files with 27 additions and 37 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
Isabelle_DOF/thys/manual/03_GuidedTour.thy
View File

@ -85,8 +85,9 @@ subsection*[document::example]\<open>Document Generation\<close>
text\<open>\<^isadof> provides an enhanced setup for generating PDF document. In particular, it does text\<open>\<^isadof> provides an enhanced setup for generating PDF document. In particular, it does
not make use of a file called \<^verbatim>\<open>document/root.tex\<close>. Instead, the use of document templates and not make use of a file called \<^verbatim>\<open>document/root.tex\<close>. Instead, the use of document templates and
ontology represenations is done within theory files. To make use of this feature, one needs ontology represenations is done within theory files. To make use of this feature, one needs
to add the option \<^verbatim>\<open>document_build = dof\<close> to the \<^verbatim>\<open>ROOT\<close> file. An example \<^verbatim>\<open>ROOT\<close> file looks to add the option \<^verbatim>\<open>document_build = dof\<close> to the \<^verbatim>\<open>ROOT\<close> file.
as follows: An example \<^verbatim>\<open>ROOT\<close> file looks as follows:
\begin{config}{ROOT} \begin{config}{ROOT}
session example = HOL + session example = HOL +
options [document = pdf, document_output = "output", document_build = dof] options [document = pdf, document_output = "output", document_build = dof]

59
Isabelle_DOF/thys/manual/04_RefMan.thy
View File

@ -502,10 +502,9 @@ text\<open>
section\<open>The Standard Ontology Libraries\<close> section\<open>The Standard Ontology Libraries\<close>
text\<open> We will describe the backbone of the Standard Library with the text\<open> We will describe the backbone of the Standard Library with the
already mentioned hierarchy \<^verbatim>\<open>COL\<close> (the common ontology library), already mentioned hierarchy \<^verbatim>\<open>COL\<close> (the common ontology library),
\<^verbatim>\<open>scholarly_paper\<close> (for MINT-oriented scientific papers), \<^verbatim>\<open>scholarly_paper\<close> (for MINT-oriented scientific papers) or
\<^verbatim>\<open>technical_report\<close> (for MINT-oriented technical reports), and \<^verbatim>\<open>technical_report\<close> (for MINT-oriented technical reports).
the example for a domain-specific ontology \<close>
\<^verbatim>\<open>CENELEC_50128\<close>.\<close>
subsection\<open>Common Ontology Library (COL)\<close> subsection\<open>Common Ontology Library (COL)\<close>
(*<*) (*<*)
@ -1184,19 +1183,14 @@ text\<open>
\begin{minipage}{.9\textwidth}\footnotesize \begin{minipage}{.9\textwidth}\footnotesize
\dirtree{% \dirtree{%
.1 . .1 .
.2 src. .2 ontologies\DTcomment{Ontologies}.
.3 ontologies\DTcomment{Ontologies}. .3 ontologies.thy\DTcomment{Ontology Registration}.
.4 ontologies.thy\DTcomment{Ontology Registration}. .3 scholarly\_paper\DTcomment{scholarly\_paper}.
.4 scholarly\_paper\DTcomment{scholarly\_paper}. .4 scholarly\_paper.thy.
.5 scholarly\_paper.thy. .4 DOF-scholarly\_paper.sty.
.5 DOF-scholarly\_paper.sty. .3 technical\_report\DTcomment{technical\_paper}.
.4 technical\_report\DTcomment{technical\_paper}. .4 technical\_report.thy.
.5 technical\_report.thy. .4 DOF-technical\_report.sty.
.5 DOF-technical\_report.sty.
.4 CENELEC\_50128\DTcomment{CENELEC\_50128}.
.5 CENELEC\_50128.thy.
.5 DOF-CENELEC\_50128.sty.
.4 \ldots.
} }
\end{minipage} \end{minipage}
\end{center} \end{center}
@ -1204,16 +1198,13 @@ text\<open>
text\<open> text\<open>
Developing a new ontology ``\<^boxed_bash>\<open>foo\<close>'' requires the Developing a new ontology ``\<^boxed_bash>\<open>foo\<close>'' requires the
following steps: following steps:
\<^item> create a new sub-directory \<^boxed_bash>\<open>foo\<close> in the directory \<^boxed_bash>\<open>ontologies\<close>
\<^item> definition of the ontological concepts, using \<^isadof>'s Ontology Definition Language (ODL), in \<^item> definition of the ontological concepts, using \<^isadof>'s Ontology Definition Language (ODL), in
a new theory file \<^path>\<open>ontologies/foo/foo.thy\<close>. a new theory file \<^path>\<open>ontologies/foo/foo.thy\<close>.
\<^item> definition of the document representation for the ontological concepts in a \LaTeX-style \<^item> definition of the document representation for the ontological concepts in a \LaTeX-style
file \<^path>\<open>ontologies/foo/DOF-foo.sty\<close> stored in the same directory as the theory file containing the ODL definitions. The file name should
\<^item> registration (as import) of the new ontology in the file \<^path>\<open>ontologies/ontologies.thy\<close>. start with the prefix ``DOF-``. For instance: \<^path>\<open>DOF-foo.sty\<close>
\<^item> activation of the new document setup by executing the install script. You can skip the lengthy \<^item> registration of the \LaTeX-style by adding a suitable \<^theory_text>\<open>define_ontology\<close>
checks for the AFP entries and the installation of the Isabelle patch by using the command to the theory containing the ODL definitions.
\<^boxed_bash>\<open>--skip-afp\<close> option:
@{boxed_bash [display] \<open>ë\prompt{\isadofdirn}ë ./install --skip-afp\<close>}
\<close> \<close>
subsection\<open>Document Templates\<close> subsection\<open>Document Templates\<close>
@ -1226,12 +1217,11 @@ text\<open>
\begin{minipage}{.9\textwidth}\footnotesize \begin{minipage}{.9\textwidth}\footnotesize
\dirtree{% \dirtree{%
.1 . .1 .
.2 src. .2 document-templates\DTcomment{Document templates}.
.3 document-templates\DTcomment{Document templates}. .3 root-lncs.tex.
.4 root-lncs.tex. .3 root-scrartcl.tex.
.4 root-scrartcl.tex. .3 root-scrreprt-modern.tex.
.4 root-scrreprt-modern.tex. .3 root-scrreprt.tex.
.4 root-scrreprt.tex.
} }
\end{minipage} \end{minipage}
\end{center} \end{center}
@ -1240,7 +1230,8 @@ text\<open>
text\<open> text\<open>
Developing a new document template ``\<^boxed_bash>\<open>bar\<close>'' requires the following steps: Developing a new document template ``\<^boxed_bash>\<open>bar\<close>'' requires the following steps:
\<^item> develop a new \<^LaTeX>-template \<^boxed_bash>\<open>src/document-templates/root-bar.tex\<close> \<^item> develop a new \<^LaTeX>-template \<^boxed_bash>\<open>src/document-templates/root-bar.tex\<close>
\<^item> add a suitable \<^theory_text>\<open>define_template\<close> command to theory \<^theory>\<open>Isabelle_DOF.Isa_DOF\<close>. \<^item> add a suitable \<^theory_text>\<open>define_template\<close> command to a theory that is
imported by the project that shall use the new document template.
\<close> \<close>
@ -1332,10 +1323,8 @@ text\<open>
requires that information is written into an auxiliary file during the first run of \<^LaTeX> requires that information is written into an auxiliary file during the first run of \<^LaTeX>
so that the information is available at further runs of \<^LaTeX>. While, on the one hand, so that the information is available at further runs of \<^LaTeX>. While, on the one hand,
this is a standard process (\<^eg>, used for updating references), implementing it correctly this is a standard process (\<^eg>, used for updating references), implementing it correctly
requires a solid understanding of \<^LaTeX>'s expansion mechanism. In this context, the recently requires a solid understanding of \<^LaTeX>'s expansion mechanism.
introduced \inlineltx|\expanded{}|-primitive Examples of this can be found, \<^eg>, in the ontology-style
(see \<^url>\<open>https://www.texdev.net/2018/12/06/a-new-primitive-expanded\<close>) is particularly useful.
Examples of its use can be found, \<^eg>, in the ontology-style
\<^file>\<open>../../ontologies/scholarly_paper/DOF-scholarly_paper.sty\<close>. \<^file>\<open>../../ontologies/scholarly_paper/DOF-scholarly_paper.sty\<close>.
For details about the expansion mechanism For details about the expansion mechanism
in general, we refer the reader to the \<^LaTeX> literature (\<^eg>,~@{cite "knuth:texbook:1986" in general, we refer the reader to the \<^LaTeX> literature (\<^eg>,~@{cite "knuth:texbook:1986"