From 7bff41cfa8b172fac4948cbcb83f9194e79337e4 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sat, 10 Aug 2019 23:06:35 +0100 Subject: [PATCH] Moved and revised COL description. --- .../Isabelle_DOF-Manual/04_RefMan.thy | 145 ++++++++---------- .../document/lstisadof-manual.sty | 1 + .../Isabelle_DOF-Manual/document/preamble.tex | 1 + 3 files changed, 63 insertions(+), 84 deletions(-) diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy index c59390ff..14fc74d5 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy @@ -309,6 +309,29 @@ text\ within Isabelle's \LaTeX-setup. \ +subsubsection\Common Ontology Library (COL)\ +text\ + \isadof provides a Common Ontology Library (COL)\index{Common Ontology Library@see COL}\bindex{COL} + that introduces ontology concepts that are so generic that they we expect them to be useful for + all types of documents. In particular it defines the super-class \inlineisar|text_element|: the + root of all text-elements, + +\begin{isar} +doc_class text_element = + level :: "int option" <= "None" + referentiable :: bool <= "False" + variants :: "String.literal set" <= "{STR ''outline'', STR ''document''}" +\end{isar} + + Here, \inlineisar|level| defines the section-level (\eg, using a \LaTeX-inspired hierarchy: + from \inlineisar|Some -1| (corresponding to \inlineltx|\part|) to + \inlineisar|Some 0| (corresponding to \inlineltx|\chapter|, respectively, \inlineisar|chapter*|) + to \inlineisar|Some 3| (corresponding to \inlineltx|\subsubsection|, respectively, + \inlineisar|subsubsection*|). Using an invariant, a derived ontology could, \eg, require that + any sequence of technical-elements must be introduced by a text-element with a higher level + (this would require that technical text section are introduce by a section element). +\ + subsubsection\Example\ text\ The category ``exported constraint (EC)'' is, in the file @@ -324,15 +347,8 @@ doc_class EC = AC + assumption_kind :: ass_kind <= (*default *) formal \end{isar} - As this definition is part of the theory \inlineisar|CENELEC_50128|, the full-quallified - name of the document class is \inlineisar|t$$ext.CENELEC_50128.EC| and, \eg, the full-qualified - name of the attribute \inlineisar|long_name|, inherited from the document class - \inlineisar|requirement|, is \inlineisar|CENELEC_50128.requirement.long_name|. - - Let us assume that we want to register the ECs in a dedicated table of contents (\inlineltx{tos}) - and use an earlier defined environment \inlineltx|\begin{EC}...\end{EC}| for the graphical - representation. We can implement this the corresponding document representation in - \path{ontologies/CENELEC_50128/DOF-CENELEC_50128.sty} as follows: + We now define the document representations, in the file + \path{ontologies/CENELEC_50128/DOF-CENELEC_50128.sty}, as follows: \begin{ltx} \newisadof{text.CENELEC_50128.EC}% @@ -366,6 +382,13 @@ doc_class EC = AC + } \end{ltx} + This definition registers the ECs in a dedicated table of contents (\inlineltx{tos}) + and uses an earlier defined environment \inlineltx|\begin{EC}...\end{EC}| for the graphical + representation. Note that this definitions requires teh full-qualified names, \eg, + \inlineisar|t$$ext.CENELEC_50128.EC| for the document class and + \inlineisar|CENELEC_50128.requirement.long_name| for the attribute \inlineisar|long_name|, + inherited from the document class \inlineisar|requirement|. + While arbitrary \LaTeX-commands can be used within the \inlineltx|\newisadof|-command, special care is required for arguments containing special characters (\eg, the underscore ``\_'') that do have a special meaning in \LaTeX. @@ -384,7 +407,34 @@ text\ While the default user interface for class definitions via the \inlineisar|text*\ ... \|-command allow to access all features of the document class, \isadof provides short-hands for certain, widely-used, concepts such as - \inlineisar|title*\ ... \| or \inlineisar|section*\ ... \|. + \inlineisar|title*\ ... \| or \inlineisar|section*\ ... \|, \eg: + +\begin{isar} +title*[title::title]\Isabelle/DOF\ +subtitle*[subtitle::subtitle]\User and Implementation Manual\ +text*[adb:: author, + email="\a.brucker@exeter.ac.uk\", + orcid="\0000-0002-6355-1200\", + http_site="\https://www.brucker.ch/\", + affiliation="\University of Exeter, Exeter, UK\"] + \Achim D. Brucker\ +text*[bu::author, + email = "\wolff@lri.fr\", + affiliation = "\Université Paris-Saclay, LRI, Paris, France\"] + \Burkhart Wolff\ +\end{isar} + + In general, all standard text-elements from the Isabelle document model such + as @{command "chapter"}, @{command "section"}, @{command "text"}, have in the \isadof + implementation their counterparts in the family of text-elements that are "ontology-aware", + \ie they dispose on a meta-argument list that allows to define that a test-element + \<^enum> has an identity as a text-object labelled as \obj_id\ + \<^enum> belongs to a document class \class_id\ that has been defined earlier + \<^enum> has its class-attributes set with particular values + (which are denotable in Isabelle/HOL mathematical term syntax) + +\clearpage + \<^item> \annotated_text_element\ : \<^rail>\ ( ( @@{command "title*"} @@ -403,6 +453,7 @@ text\ | change_status_command | inspection_command \ +\clearpage \<^item> \meta_args\ : \<^rail>\(obj_id ('::' class_id) ((attribute '=' term)) * ',')\ \<^item> \rich_meta_args\ : @@ -625,80 +676,6 @@ programming involves a deeper understanding of ontology modeling and the \ -section*["core-manual"::technical]\Annotatable Text-Elements for Core-Documents\ -text\In general, all standard text-elements from the Isabelle document model such -as @{command "chapter"}, @{command "section"}, @{command "text"}, have in the \isadof -implementation their counterparts in the family of text-elements that are "ontology-aware", -\ie they dispose on a meta-argument list that allows to define that a test-element -\<^enum> has an identity as a text-object labelled as \obj_id\ -\<^enum> belongs to a document class \class_id\ that has been defined earlier -\<^enum> has its class-attributes set with particular values - (which are denotable in Isabelle/HOL mathematical term syntax) -\ - -subsection\Annotating with Ontology Meta-Data: Outer Syntax\ -text\\dof introduces its own family of text-commands, which allows -having side effects of the global context \inlineisar+\+ and thus to -store and manage own meta-information. Among others, \dof provides the commands -\inlineisar+section*[]\...\+, -\inlineisar+subsection*[]\...\Cclose>+, or -\inlineisar+text*[]\...\+. Here, the argument -\inlineisar++ is a syntax for declaring instance, class and -attributes for this text element, following the scheme -\begin{isar} - :: , attr_1 = , ..., attr_n = -\end{isar} -The \inlineisar++ can be omitted, which -represents the implicit superclass \inlineisar+text+, where -\inlineisar+attr_i+ must be declared attributes in the class and where -the HOL \inlineisar++ must have the corresponding HOL type. Attributes -from a class definition may be left undefined; definitions of -attribute values \<^emph>\override\ default values or values of -super-classes. Overloading of attributes is not permitted in -\dof. -\ - - -subsection*["commonlib"::technical]\Common Ontology Library (COL)\ -text\ The COL library is used to capture a couple of text-elements -that are expected to be common to all document types, a class -that is actually not easy to define. After a lot of thought, we excluded -things like @{command "title*"} and abstract-related classes back again -to specific ontologies, for example. - -Finally, it is currently reduced to -\<^enum> the common infra-structure on text-elements (section is a text-element of a certain "level"), -\<^enum> common infrastructure to semi-formal Isabelle elements (Definitions, Assertions, Proofs), and -\<^enum> the common infra-structure for figures. - -Future extensions might include, for example, the infra-structure for tables. -\ - -text\ The super-class \<^verbatim>\text_element\ is the root of all text-elements used in \isadof. -It is defined as follows: -\begin{isar} -doc_class text_element = - level :: "int option" <= "None" - referentiable :: bool <= "False" - variants :: "String.literal set" <= "{STR ''outline'', STR ''document''}" -\end{isar} -Of major importance is the @{term "level"} which influences, inspired by a LaTeX convention, -the following classification: -\<^enum> part = Some -1 -\<^enum> chapter = Some 0 -\<^enum> section = Some 1 -\<^enum> subsection = Some 2 -\<^enum> subsubsection = Some 3 -\<^enum> ... -for scholarly paper: invariant level > - -The attribute @{term "level"} in the subsequent enables doc-notation --- a kind of macro --- -for support of @{command "chapter*"}, @{command "section*"} etc. This class definition forms -for a number of invariants; for example, the derived ontology \scholarly_paper\ contains an -invariant that any sequence of, for example, \technical\ - elements must be introduced -by a text-element with a higher level, \ie{}, must contain a section or subsection header. -\ - section*["document-templates"::technical]\Defining Document Templates\ diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/lstisadof-manual.sty b/examples/technical_report/Isabelle_DOF-Manual/document/lstisadof-manual.sty index 4f3073ef..c46e2d54 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/document/lstisadof-manual.sty +++ b/examples/technical_report/Isabelle_DOF-Manual/document/lstisadof-manual.sty @@ -86,6 +86,7 @@ {}{\ensuremath{\isacartoucheopen}}1% %{<@>}{@}1% {"}{}0% + {é}{\'e}1% {~}{\ }1% {::}{:\!:}1% {}{\ensuremath{\isacartoucheclose}}1% diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex b/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex index d05e4071..56344f65 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex +++ b/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex @@ -24,6 +24,7 @@ \usepackage{xcolor} \usepackage{paralist} \usepackage{listings} +\usepackage{listingsutf8} \usepackage{lstisadof-manual} \usepackage{xspace} \usepackage{dtk-logos}