diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy index cbf4fafe..4ab8cff7 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy @@ -30,8 +30,8 @@ text\ for document-classes and all auxiliary datatypes (called Ontology Definition Language (ODL)), \<^item> the ontology-specific \<^emph>\layout definition\, exploiting this meta-information, and - \<^item> the generic \<^emph>\layout definition\ for documents following, \eg, the format guidelines of publishers - or standardization bodies. + \<^item> the generic \<^emph>\layout definition\ for documents following, \eg, the format guidelines of + publishers or standardization bodies. \ subsection\Ontologies\ @@ -204,7 +204,7 @@ text\ (called \short_id\'s in @{cite "isaisarrefman19"}) and identifiers in \inlineisar+" ... "+ which might contain certain ``quasi-letters'' such as \inlineisar+_+, \inlineisar+-+, \inlineisar+.+. See~@{cite "isaisarrefman19"} for details. - \clearpage" + \clearpage \<^item> \tyargs\:\index{tyargs@\tyargs\} \<^rail>\ typefree | ('(' (typefree * ',') ')')\ \typefree\ denotes fixed type variable(\'a\, \'b\, ...) (see~@{cite "isaisarrefman19"}) @@ -235,20 +235,21 @@ text\ \ text\ - Other specification constructs, which are potentially relevant for an (advanced) ontology - developer, might be recursive function definitions with pattern-matching~@{cite "functions19"}, - extensible record specifications~@{cite "isaisarrefman19"}, and abstract type declarations. + Advanced ontology might make use of concepts such as recursive function definitions with + pattern-matching~@{cite "functions19"}, extensible record + pecifications~@{cite "isaisarrefman19"}, and abstract type declarations. \ -subsection*["odl-manual1"::technical]\The Command Syntax for Document Class Specifications\ +subsection*["odl-manual1"::technical]\Defining Document Classes\ text\ -\<^item> \class_id\:\index{class\_id@\class_id\} a \class_id\ is a type-\name\ that has been introduced +A document class\bindex{document class} can be defined using the @{command "doc_class"} keyword: +\<^item> \class_id\:\index{class\_id@\class_id\} a type-\name\ that has been introduced via a \doc_class_specification\. \<^item> \doc_class_specification\:\index{doc\_class\_specification@\doc_class_specification\} \<^rail>\ @@{command "doc_class"} class_id '=' (class_id '+')? (attribute_decl+) \ (accepts_clause rejects_clause?)?\ - document classes whose specification contains an \accepts_clause\ are called + Document classes whose specification contains an \accepts_clause\ are called \<^emph>\monitor classes\ or \<^emph>\monitors\ for short. \<^item> \attribute_decl\:\index{attribute\_decl@\attribute_decl\} \<^rail>\ name '::' '"' type '"' default_clause? \ @@ -266,25 +267,90 @@ text\ repetitions and non-empty sequence follow in the top-down order of the above diagram. \ - text\ + \isadof provides a default document representation (\ie, content and layout of the generated + PDF) that only prints the main text, omitting all attributes. \isadof provides the + \inlineltx|\newisadof[]{}|\index{newisadof@\inlineltx{\newisadof}}\index{document class!PDF} + command for defining a dedicated layout for a document class in \LaTeX. Such a document + class-specific \LaTeX-definition can not only provide a specific layout (\eg, a specific + highlighting, printing of certain attributes), it can also generate entries in in the table of + contents or an index. Overall, the \inlineltx|\newisadof[]{}| command follows the structure + of the \inlineisar|doc_class|-command: + +\begin{ltx}[escapechar=ë] +\newisadof{ë\class_id\ë}[label=,type=, ë\attribute_decl\ë][1]{% + % ë\LaTeXë-definition of the document class representation + \begin{isamarkuptext}% + #1% + \end{isamarkuptext}% +} +\end{ltx} + + The \class_id\ is the full-qualified name of the document class and the list of \attribute_decl\ + needs to declare all attributes of the document class. Within the \LaTeX-definition of the document + class representation, the identifier \inlineltx|#1| refers to the content of the main text of the + document class (written in \inlineisar|\ ... \|) and the attributes can be referenced + by their name using the \inlineltx|\commandkey{...}|-command (see the documentation of the + \LaTeX-package ``keycommand''~@{cite "chervet:keycommand:2010"} for details). Usually, the + representations definition needs to be wrapped in a + \inlineltx|\begin{isarmarkup}...\end{isamarkup}|-environment, to ensure the correct context + within Isabelle's \LaTeX-setup. +\ + +subsubsection\Example\ +text\ + The category ``exported constraint (EC)'' is, in the file + \path{ontologies/CENELEC_50128/CENELEC_50128.thy} defined as follows: + +\begin{isar} +doc_class requirement = text_element + + long_name :: "string option" + is_concerned :: "role set" +doc_class AC = requirement + + is_concerned :: "role set" <= "UNIV" +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: + \begin{ltx} -\newisadof{text.CENELEC_50128.hypothesis}% +\newisadof{text.CENELEC_50128.EC}% [label=,type=% ,Isa_COL.text_element.level=% ,Isa_COL.text_element.referentiable=% ,Isa_COL.text_element.variants=% ,CENELEC_50128.requirement.is_concerned=% ,CENELEC_50128.requirement.long_name=% -,CENELEC_50128.SRAC.formal_repr=% -,CENELEC_50128.SRAC.hypothesis_kind=% -,CENELEC_50128.hypothesis.hyp_type=% -][1]{ -#1 +,CENELEC_50128.EC.assumption_kind=% +][1]{% +\begin{isamarkuptext}% + \ifthenelse{\equal{\commandkey{CENELEC_50128.requirement.long_name}}{}}{% + \begin{EC}% + \addxcontentsline{tos}{chapter}[]{\autoref{\commandkey{label}}}% + }{% + \begin{EC}[\commandkey{CENELEC_50128.requirement.long_name}]% + \addxcontentsline{toe}{chapter}[]{\autoref{\commandkey{label}}: % + \commandkey{CENELEC_50128.requirement.long_name}}% + \DOFindex{EC}{\commandkey{CENELEC_50128.requirement.long_name}}% + }\label{\commandkey{label}}% + #1% + \end{EC} +\end{isamarkuptext}% } \end{ltx} \ + + subsection*["core-manual1"::technical]\Annotatable Test-Elements: Syntax\ text\The syntax of toplevel \isadof commands reads as follows: diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/root.bib b/examples/technical_report/Isabelle_DOF-Manual/document/root.bib index e77431af..40c1d21d 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/document/root.bib +++ b/examples/technical_report/Isabelle_DOF-Manual/document/root.bib @@ -599,3 +599,10 @@ title={The Isabelle System Manual}, year = 2019 } + +@Booklet{ chervet:keycommand:2010, + author={Florent Chervet}, + title={The free and open source keycommand package: key-value interface + for commands and environments in {\LaTeX}.}, + year = 2010 +}