Theory M_06_RefMan

(*************************************************************************
 * Copyright (C) 
 *               2019-2022 University of Exeter 
 *               2018-2022 University of Paris-Saclay
 *               2018      The University of Sheffield
 *
 * License:
 *   This program can be redistributed and/or modified under the terms
 *   of the 2-clause BSD-style license.
 *
 *   SPDX-License-Identifier: BSD-2-Clause
 *************************************************************************)

(*<*)
theory 
  "M_06_RefMan"
  imports 
    "M_05_Proofs_Ontologies" 
begin

declare_reference*[infrastructure::technical]

(*>*)

chapter*[isadof_ontologies::technical]‹Ontologies and their Development›

text‹
  In this chapter, we explain the concepts of isadof in a more systematic way, and give
  guidelines for modeling new ontologies, present underlying concepts for a mapping to a
  representation, and give hints for the development of new document templates. 

  isadof is embedded in the underlying generic document model of Isabelle as described in
  @{scholarly_paper.introduction ‹dof›}. Recall that the document language can be extended dynamically, ie, new
  ∗‹user-defined› can be introduced at run-time.  This is similar to the definition of new functions 
  in an interpreter. isadof as a system plugin provides a number of new command definitions in 
  Isabelle's document model.

  isadof consists consists basically of five components:
  ▪ the ∗‹core› in theory‹Isabelle_DOF.Isa_DOF› providing the ∗‹ontology definition language›
    (ODL) which allow for the definitions of document-classes
    and necessary datatypes,
  ▪ the ∗‹core› also provides an own ∗‹family of commands› such as 
    boxed_theory_text‹text*›, boxed_theory_text‹ML*›, boxed_theory_text‹value*› , etc.;
    They allow for the annotation of document-elements with meta-information defined in ODL,
  ▪ the isadof library theory‹Isabelle_DOF.Isa_COL› providing
    ontological basic (documents) concepts bindex‹ontology› as well as supporting infrastructure, 
  ▪ an infrastructure for ontology-specific ∗‹layout definitions›, exploiting this meta-information, 
    and 
  ▪ an infrastructure for generic ∗‹layout definitions› for documents following, eg, the format 
    guidelines of publishers or standardization bodies. 
›
text‹
  Similarly to Isabelle, which is based on a core logic theory‹Pure› and then extended by libraries
  to major systems like ▩‹HOL›, isadof has a generic core infrastructure dof and then presents 
  itself to users via major library extensions,  which add domain-specific  system-extensions. 
  Ontologiesbindex‹ontology› in isadof are not just a sequence of descriptions in isadof's Ontology 
  Definition Language (ODL)bindex‹ODL›. Rather, they are themselves presented as integrated 
  sources that provide textual descriptions, abbreviations, macro-support and even ML-code. 
  Conceptually, the library of isadof is currently organized as follows⁋‹The ∗‹technical› 
  organization is slightly different and shown in 
  @{technical (unchecked) ‹infrastructure›}.›
  bindex‹COL›bindex‹scholarly\_paper›bindex‹technical\_report› bindex‹CENELEC›: 
%
latex‹
\begin{center}
\begin{minipage}{.9\textwidth}\footnotesize
\dirtree{%
.1 COL\DTcomment{The Common Ontology Library}.
.2 scholarly\_paper\DTcomment{Scientific Papers}.
.3 technical\_report\DTcomment{Extended Papers, Technical Reports}.
.4 CENELEC\_50128\DTcomment{Papers according to CENELEC\_50128}.
.4 CC\_v3\_1\_R5\DTcomment{Papers according to Common Criteria}. 
.4 \ldots.
}
\end{minipage}
\end{center}›

 These libraries not only provide ontological concepts, but also syntactic sugar in Isabelle's
 command language Isar that is of major importance for users (and may be felt as isadof key 
 features by many authors). In reality, 
 they are derived concepts from more generic ones; for example, the commands
 boxed_theory_text‹title*›, boxed_theory_text‹section*›,  boxed_theory_text‹subsection*›, etc,
 are in reality a kind of macros for boxed_theory_text‹text*[<label>::title]...›,
 boxed_theory_text‹text*[<label>::section]...›, respectively.
 These example commands are defined in ▩‹COL› (the common ontology library).

 As mentioned earlier, our ontology framework is currently particularly geared towards 
 ∗‹document› editing, structuring and presentation (future applications might be advanced
 "knowledge-based" search procedures as well as tool interaction). For this reason, ontologies
 are coupled with ∗‹layout definitions› allowing an automatic mapping of an integrated
 source into LaTeX and finally pdf. The mapping of an ontology to a specific representation
 in LaTeX is steered via associated  LaTeX style files which were included during Isabelle's
 document generation process. This mapping is potentially a one-to-many mapping;
 this implies a certain technical organization and some resulting restrictions 
 described in @{technical (unchecked) ‹infrastructure›} in more detail.
›

section‹The Ontology Definition Language (ODL)›
text‹
 ODL shares some similarities with meta-modeling languages such as UML class 
 models: It builds upon concepts like class, inheritance, class-instances, attributes, references 
 to instances, and class-invariants. Some concepts like  advanced type-checking, referencing to 
 formal entities of Isabelle, and monitors are due to its specific application in the 
 Isabelle context. Conceptually, ontologies specified in ODL consist of:
    ▪ ∗‹document classes› (boxed_theory_text‹doc_class›) index‹doc\_class› that describe concepts,
      the keyword (boxed_theory_text‹onto_class›) index‹onto\_class› is syntactically equivalent,
    ▪ an optional document base class expressing single inheritance  class extensions,
      restricting the class-hierarchy basically to a tree,
    ▪ ∗‹attributes› specific to document classes, where
      ▪ attributes are HOL-typed,
      ▪ attributes of instances of document elements are mutable,
      ▪ attributes can refer to other document classes, thus, document
        classes must also be HOL-types (such attributes are called  ∗‹links›),
      ▪ attribute values were denoted by HOL-terms,
    ▪ a special link, the reference to a super-class, establishes an
      ∗‹is-a› relation between classes,
    ▪ classes may refer to other classes via a regular expression in an
      ∗‹accepts› clause, or via a list in a ∗‹rejects› clause,
    ▪ attributes may have default values in order to facilitate notation.

boxed_theory_text‹doc_class›'es and boxed_theory_text‹onto_class›'es respectively, have a semantics,
ie, a logical representation as extensible records in HOL (cite‹"wenzel:isabelle-isar:2020"›, 
pp. 11.6); there are therefore amenable to logical reasoning.
›

text‹
  The isadof ontology specification language consists basically of a notation for document classes, 
  where the attributes were typed with HOL-types and can be instantiated by HOL-terms, ie, 
  the actual parsers and type-checkers of the Isabelle system were reused. This has the particular 
  advantage that isadof commands can be arbitrarily mixed with Isabelle/HOL commands providing the 
  machinery for type declarations and term specifications such
  as enumerations. In particular, document class definitions provide:
  ▪ a HOL-type for each document class as well as inheritance, 
  ▪ support for attributes with HOL-types and optional default values,
  ▪ support for overriding of attribute defaults but not overloading, and
  ▪ text-elements annotated with document classes; they are mutable 
    instances of document classes.
›

text‹
  Attributes referring to other ontological concepts are called ∗‹links›. The HOL-types inside the 
  document specification language support built-in types for Isabelle/HOL boxed_theory_text‹typ›'s,  
  boxed_theory_text‹term›'s, and boxed_theory_text‹thm›'s reflecting internal Isabelle's  internal 
  types for these entities; when denoted in HOL-terms to instantiate an attribute, for example, 
  there is a  specific syntax (called ∗‹term antiquotations›) that is checked by 
  isadof for consistency.

  Document classesbindex‹document class›index‹class!document@see document class› support 
  boxed_theory_text‹accepts›-clausesindex‹accepts\_clause@‹accepts_clause›› containing
  a regular expression over class names.
  Classes with an boxed_theory_text‹accepts›-clause were called 
  ∗‹monitor classes›.bindex‹monitor class›index‹class!monitor@see monitor class› While document 
  classes and their inheritance relation structure meta-data of text-elements in an object-oriented 
  manner, monitor classes enforce structural organization of documents via the language specified 
  by the regular expression enforcing a sequence of text-elements.

  A major design decision of ODL is to denote attribute values by HOL-terms and HOL-types. 
  Consequently, ODL can refer to any predefined type defined in the HOL library, eg, 
  typ‹string› or typ‹int› as well as parameterized types, eg,
  typ‹_ option›, typ‹_ list›, typ‹_ set›, or products
  typ‹_ × _›. As a consequence of the 
  document model, ODL definitions may be arbitrarily intertwined with standard HOL type definitions. 
  Finally, document class definitions result in themselves in a HOL-type in order to allow ∗‹links› 
  to and between ontological concepts.
›

subsection*["odl_manual0"::technical]‹Some Isabelle/HOL Specification Constructs Revisited›
text‹
  As ODL is an extension of Isabelle/HOL, document class definitions can therefore be arbitrarily 
  mixed with standard HOL specification constructs. To make this manual self-contained, we present 
  syntax and semantics of the specification constructs that are most likely relevant for the 
  developer of ontologies (for more details, see~cite‹"wenzel:isabelle-isar:2020"›).  Our 
  presentation is a simplification of the original sources following the needs of ontology developers 
  in isadof:
  ▪ ‹name›:index‹name@‹name››
     with the syntactic category of ‹name›'s we refer to alpha-numerical identifiers 
     (called ‹short_ident›'s in cite‹"wenzel:isabelle-isar:2020"›) and identifiers
     in boxed_theory_text‹...› which might contain certain ``quasi-letters'' such 
     as boxed_theory_text‹_›, boxed_theory_text‹-›, boxed_theory_text‹.› (see~cite‹"wenzel:isabelle-isar:2020"› for 
     details).
       % TODO
       % This phrase should be reviewed to clarify identifiers.
       % Peculiarly, "and identifiers in boxed_theory_text‹ ... ›". 
  ▪ ‹tyargs›:index‹tyargs@‹tyargs›› 
     rail‹  typefree | ('(' (typefree * ',') ')')›
     ‹typefree› denotes fixed type variable (‹'a›, ‹'b›, ...) (see~cite‹"wenzel:isabelle-isar:2020"›)
  ▪ ‹dt_name›:index‹dt\_npurdahame@‹dt_name››
     rail‹  (tyargs?) name (mixfix?)›   
     The syntactic entity ‹name› denotes an identifier, ‹mixfix› denotes the usual 
     parenthesized mixfix notation (see cite‹"wenzel:isabelle-isar:2020"›).
     The ∗‹name›'s referred here are type names such as typ‹int›, typ‹string›,
     type‹list›, type‹set›, etc. 
  ▪ ‹type_spec›:\index{type_spec@‹type_spec›}
     rail‹  (tyargs?) name›
     The ∗‹name›'s referred here are type names such as typ‹int›, typ‹string›,
     type‹list›, type‹set›, etc. 
  ▪ ‹type›:index‹type@‹type››
     rail‹  (( '(' ( type * ',')  ')' )? name) | typefree ›     
  ▪ ‹dt_ctor›:index‹dt\_ctor@‹dt_ctor››
     rail‹ name (type*) (mixfix?)›
  ▪ ‹datatype_specification›:index‹datatype\_specification@‹datatype_specification››
     rail‹ @@{command "datatype"} dt_name '=' (dt_ctor * '|' )›
  ▪ ‹type_synonym_specification›:index‹type\_synonym\_specification@‹type_synonym_specification››
     rail‹ @@{command "type_synonym"} type_spec '=' type›
  ▪ ‹constant_definition› :index‹constant\_definition@‹constant_definition››
     rail‹ @@{command "definition"} name '::' type 'where' '"' name '=' ⏎ expr '"'›
  ▪ ‹expr›:index‹expr@‹expr››
     the syntactic category ‹expr› here denotes the very rich language of 
     mathematical  notations encoded in ‹λ›-terms in Isabelle/HOL. Example expressions are:
     boxed_theory_text‹1+2› (arithmetics), boxed_theory_text‹[1,2,3]› (lists), boxed_theory_text‹ab c› (strings),
     % TODO
     % Show string in the document output for  boxed_theory_text‹ab c› (strings) 
     boxed_theory_text‹{1,2,3}› (sets), boxed_theory_text‹(1,2,3)› (tuples), 
     boxed_theory_text‹∀ x. P(x) ∧ Q x = C› (formulas). For comprehensive overview, 
     see~cite‹"nipkow:whats:2020"›.
›

text‹
  Advanced ontologies can, eg,  use recursive function definitions with 
  pattern-matching~cite‹"kraus:defining:2020"›, extensible record 
  specifications~cite‹"wenzel:isabelle-isar:2020"›, and abstract type declarations.
›

text‹isadof works internally with fully qualified names in order to avoid confusions 
occurring otherwise, for example, in disjoint class hierarchies. This also extends to names for
 boxed_theory_text‹doc_class›es, which must be representable as type-names as well since they
can be used in attribute types. Since theory names are lexically very liberal 
(boxed_theory_text‹0.thy› is a legal theory name), this can lead to subtle problems when 
constructing a class: boxed_theory_text‹foo› can be a legal name for a type definition, the 
corresponding type-name boxed_theory_text‹0.foo› is not. For this reason, additional checks at the 
definition of a boxed_theory_text‹doc_class› reject problematic lexical overlaps.›


subsection*["odl_manual1"::technical]‹Defining Document Classes›
text‹
A document classbindex‹document class› can be defined using the @{command "doc_class"} keyword: 
▪ ‹class_id›:bindex‹class\_id@‹class_id›› a type-‹name› that has been introduced 
  via a ‹doc_class_specification›.
▪ ‹doc_class_specification›:index‹doc\_class\_specification@‹doc_class_specification››
     We call document classes with an ‹accepts_clause› 
     ∗‹monitor classes› or ∗‹monitors› for short.
     rail‹ (@@{command "doc_class"}| @@{command "onto_class"}) class_id '=' (class_id '+')? (attribute_decl+) ⏎
           (invariant_decl *) (rejects_clause accepts_clause)? ⏎ (accepts_clause *)›
▪ ‹attribute_decl›:index‹attribute\_decl@‹attribute_decl››
     rail‹ name '::' '"' type '"' default_clause? ›
▪ ‹invariant_decl›:index‹invariant\_decl@‹invariant_decl››
     Invariants can be specified as predicates over document classes represented as 
     records in HOL. Sufficient type information must be provided in order to
     disambiguate the argument of the expression
     and the boxed_text‹σ› symbol is reserved to reference the instance of the class itself. 
     rail‹ 'invariant' (name '::' '"' term '"' + 'and') ›
▪ ‹rejects_clause›:index‹rejects\_clause@‹rejects_clause››
     rail‹ 'rejects' (class_id * ',') ›
▪ ‹accepts_clause›:index‹accepts\_clause@‹accepts_clause››
     rail‹ 'accepts' ('"' regexpr '"' + 'and')›
▪ ‹default_clause›:index‹default\_clause@‹default_clause›› 
     rail‹ '<=' '"' expr '"' ›
▪ ‹regexpr›:index‹regexpr@‹regexpr››
     rail‹ '⌊' class_id '⌋' | '(' regexpr ')' | (regexpr '||' regexpr) | (regexpr '~~' regexpr)
            | ('⦃' regexpr '⦄+') | ( '⦃' regexpr '⦄*')  ›
     % TODO
     % Syntax for class_id does not seem to work (⌊ and ⌋ do not work)
     Regular expressions describe sequences of ‹class_id›s (and indirect sequences of document
     items corresponding to the ‹class_id›s). The constructors for alternative, sequence, 
     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 
  ltxinline‹\newisadof[]{}›index‹newisadof@boxed_latex‹\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 the table of 
  contents or an index. Overall, the  ltxinline‹\newisadof[]{}› command follows the structure
  of the boxed_theory_text‹doc_class›-command:

% bu: not embeddable macro: too many guillemots ...
\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› (or ∗‹cid›index‹cid!cid@‹see class_id›› for short) 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 boxed_latex‹#1› refers to the content of the main text of the 
  document class (written in boxed_theory_text‹‹ ... ››) and the attributes can be referenced
  by their name using the  ltxinline‹\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 
  ltxinline‹\begin{isarmarkup}...\end{isamarkup}›-environment, to ensure the correct context 
  within Isabelle's LaTeX-setup. 
  % TODO:
  % Clarify \newisadof signature: \newisadof[]{} vs \newisadof{}[]{}.
  Moreover, isadof also provides the following two variants of \inlineltx|\newisadof{}[]{}|:
  ▪  ltxinline‹\renewisadof{}[]{}›index‹renewisadof@boxed_latex‹\renewisadof›› for re-defining 
     (over-writing) an already defined command, and  
  ▪  ltxinline‹\provideisadof{}[]{}›index‹provideisadof@boxed_latex‹\provideisadof›› for providing 
     a definition if it is not yet defined. 
›
text‹
  While arbitrary LaTeX-commands can be used within these commands,
  special care is required for arguments containing special characters (eg, the 
  underscore ``\_'') that do have a special meaning in LaTeX.  
  Moreover, as usual, special care has to be taken for commands that write into aux-files
  that are included in a following LaTeX-run. For such complex examples, we refer the interested 
  reader to  the style files provided in the isadof distribution. In particular 
  the definitions of the concepts boxed_theory_text‹title*› and boxed_theory_text‹author*› in LaTeX-style 
  for the ontology @{theory ‹Isabelle_DOF.scholarly_paper›} shows examples of protecting 
  special characters in definitions that need to make use of a entries in an aux-file. 
›

section‹The main Ontology-aware Document Elements›
text‹Besides the core-commands to define an ontology as presented in the previous section, 
the isadof core provides a number of mechanisms to ∗‹use› the resulting data to annotate
texts, code, and terms. As mentioned already in the introduction, this boils down two three major
groups of commands used to annotate text-. code-, and term contexts with instances of ontological
classes, ie, meta-information specified in an ontology. Representatives of these three groups,
which refer by name to equivalent standard Isabelle commands by their name suffixed with a ‹*›, 
are presented as follows in a railroad diagram:

   ▪ ‹annotated_text_element› :
   rail‹( @@{command "text*"} '[' meta_args ']' '‹' text context '›' )
     ›
   ▪ ‹annotated_code_element› :
   rail‹( @@{command "ML*"} '[' meta_args ']' '‹' code context '›' )
     ›
   ▪ ‹annotated_term_element› :
   rail‹( @@{command "value*"} '[' meta_args ']' '‹' term context '›' )
     ›

In the following, we will formally introduce the syntax of the core commands as 
supported on the Isabelle/Isar level. On this basis, concepts such as the freeform 
⬚‹Definition*› and ⬚‹Lemma*› elements were derived from ⬚‹text*›. Similarly,the
corresponding formal ⬚‹definition*› and ⬚‹lemma*› elements were built on top of 
functionality of the  ⬚‹value*›-family.

›

subsection‹General Syntactic Elements for Document Management›

text‹Recall that except ⬚‹text*[]‹...››, all isadof commands were mapped to visible
layout; these commands have to be wrapped into 
 ▩‹(*<*) ... (*>*)› if this is undesired. ›

text‹

▪ ‹obj_id›:index‹obj\_id@‹obj_id›› (or ∗‹oid›index‹oid!oid@‹see obj_id›› for short) a ∗‹name›
  as specified in @{technical ‹odl_manual0›}.
▪ ‹meta_args› : 
   rail‹obj_id ('::' class_id) ((',' attribute '=' HOL_term) *) ›
▪ ∗‹evaluator›: from cite‹"wenzel:isabelle-isar:2020"›, evaluation is tried first using ML,
  falling back to normalization by evaluation if this fails. Alternatively a specific
  evaluator can be selected using square brackets; typical evaluators use the
  current set of code equations to normalize and include ‹simp› for fully
  symbolic evaluation using the simplifier, ‹nbe› for ∗‹normalization by
  evaluation› and ∗‹code› for code generation in SML.
▪ ‹upd_meta_args› :
   rail‹ (obj_id ('::' class_id) ((',' attribute (':=' | '+=') HOL_term ) * ))›

▪ ‹annotated_text_element› :
rail‹  
     (  @@{command "open_monitor*"}  
        | @@{command "close_monitor*"} 
        | @@{command "declare_reference*"} 
     ) '[' meta_args ']' 
     | change_status_command
     | inspection_command
     | macro_command
  ›
▪ isadof ‹change_status_command› :
  rail‹  (@@{command "update_instance*"} '[' upd_meta_args ']')›

With respect to the family of text elements,
⬚‹text*[oid::cid, ...] ‹ … text … › › is the core-command of isadof: it permits to create
an object of meta-data belonging to the class ⬚‹cid›index‹cid!cid@‹see class_id››.
This is viewed as the ∗‹definition› of an instance of a document class.
The class invariants were checked for all attribute values
at creation time if not specified otherwise. Unspecified attributed values were represented
by fresh free variables.
This instance object is attached to the text-element
and makes it thus ``trackable'' for  isadof, ie, it can be referenced
via the ⬚‹oid›index‹oid!oid@‹see obj_id››, its attributes
can be set by defaults in the class-definitions, or set at creation time, or modified at any
point after creation via  ⬚‹update_instance*[oid, ...]›. The ⬚‹class_id› is syntactically optional;
if ommitted, an object belongs to an anonymous superclass of all classes. 
The ⬚‹class_id› is used to generate a ∗‹class-type› in HOL; note that this may impose lexical 
restrictions as well as to name-conflicts in the surrounding logical context. 
In many cases, it is possible to use the class-type to denote the ⬚‹class_id›; this also
holds for type-synonyms on class-types.

References to text-elements can occur textually before creation; in these cases, they must be 
declared via ⬚‹declare_reference*[...]› in order to compromise to Isabelle's fundamental 
``declaration-before-use" linear-visibility evaluation principle. The forward-declared class-type
must be identical with the defined class-type.

For a declared class ⬚‹cid›, there exists a text antiquotation of the form ⬚‹ @{cid ‹oid›} ›. 
The precise presentation is decided in the ∗‹layout definitions›, for example by suitable
LaTeX-template code. Declared but not yet defined instances must be referenced with a particular
pragma in order to enforce a relaxed checking ⬚‹ @{cid (unchecked) ‹oid›} ›.
The choice of the default class in a @{command "declare_reference*"}-command
can be influenced by setting globally an attribute:
@{boxed_theory_text [display]
‹declare[[declare_reference_default_class = "definition"]]›}
Then in this example:
@{boxed_theory_text [display]‹declare_reference*[def1]›}
‹def1› will be a declared instance of the class ‹definition›. 
›

subsection‹Ontological Code-Contexts and their Management›

text‹
▪ ‹annotated_code_element›:
rail‹(@@{command "ML*"}   '[' meta_args ']' '‹' SML_code '›')›

The ⬚‹ML*[oid::cid, ...] ‹ … SML-code … ››-document elements proceed similarly:
a referentiable meta-object of class ⬚‹cid› is created, initialized with the optional 
 attributes and bound to ⬚‹oid›. In fact, the entire the meta-argument list is optional.
The SML-code is type-checked and executed 
in the context of the SML toplevel of the Isabelle system as in the corresponding 
⬚‹ML‹ … SML-code … ››-command.
Additionally, ML antiquotations were added to check and evaluate terms with
term antiquotations:
▪ ⬚‹@{term_ ‹term› }› parses and type-checks ‹term› with term antiquotations,
  for instance ⬚‹@{term_ ‹@{technical ‹odl-manual1›}›}› will parse and check
  that ‹odl-manual1› is indeed an instance of the class typ‹technical›,
▪ ⬚‹@{value_ ‹term› }› performs the evaluation of ‹term› with term antiquotations,
  for instance ⬚‹@{value_ ‹definition_list @{technical ‹odl-manual1›}›}›
  will get the value of the const‹definition_list› attribute of the instance ‹odl-manual1›.
  ⬚‹value_› may have an optional argument between square brackets to specify the evaluator:
  ⬚‹@{value_ [nbe] ‹definition_list @{technical ‹odl-manual1›}›}› forces ‹value_› to evaluate
  the term using normalization by evaluation (see cite‹"wenzel:isabelle-isar:2020"›).
›

(*<*)
doc_class A =
   level :: "int option"
   x :: int
definition*[a1::A, x=5, level="Some 1"] xx' where "xx' ≡ A.x @{A ‹a1›}" if "A.x @{A ‹a1›} = 5"

doc_class E =
   x :: "string"              <= "''qed''"

doc_class cc_assumption_test =
a :: int
text*[cc_assumption_test_ref::cc_assumption_test]‹›

definition tag_l :: "'a ⇒ 'b ⇒ 'b" where "tag_l ≡ λx y. y"

lemma* tagged : "tag_l @{cc_assumption_test ‹cc_assumption_test_ref›} AAA ⟹ AAA"
  by (simp add: tag_l_def)

find_theorems name:tagged "(_::cc_assumption_test ⇒ _ ⇒ _) _ _ ⟹_"

lemma*[e5::E] testtest : "xx + A.x @{A ‹a1›} = yy + A.x @{A ‹a1›} ⟹ xx = yy" by simp

doc_class B'_test' =
b::int

text*[b::B'_test']‹›

term*‹@{B'_test' ‹b›}›

declare_reference*["text_elements_expls"::technical]
(*>*)

subsection*["subsec_onto_term_ctxt"::technical]‹Ontological Term-Contexts and their Management›
text‹ 
▪ ‹annotated_term_element›
rail‹ 
    (@@{command "term*"} ('[' meta_args ']')? '‹' HOL_term  '›'
     | (@@{command "value*"}
        | @@{command "assert*"}) ⏎ ('[' evaluator ']')? ('[' meta_args ']')? '‹' HOL_term '›'
     | (@@{command "definition*"}) ('[' meta_args ']')?
        ('... see ref manual')
     | (@@{command "lemma*"} | @@{command "theorem*"} | @@{command "corollary*"}
       | @@{command "proposition*"} ) ('[' meta_args ']')?
         ('... see ref manual')
    )
  ›

For a declared class ⬚‹cid›, there exists a term-antiquotation of the form ⬚‹@{cid ‹oid›}›.
The major commands providing term-contexts are⁋‹The meta-argument list is optional.›
  ▪ ⬚‹term*[oid::cid, ...] ‹ … HOL-term … ››,
  ▪ ⬚‹value*[oid::cid, ...] ‹ … HOL-term … ››, and
  ▪ ⬚‹assert*[oid::cid, ...] ‹ … HOL-term … ››
  ▪ ⬚‹definition*[oid::cid, ...] const_name where ‹ … HOL-term … ››, and
  ▪ ⬚‹lemma*[oid::cid, ...] name :: ‹ … HOL-term … ››.


Wrt. creation, checking and traceability, these commands are analogous to the ontological text and
code-commands. However the argument terms may contain term-antiquotations stemming from an
ontology definition. Term-contexts were type-checked and ∗‹validated› against
the global context (so: in the term @{term_ [source] ‹@{scholarly_paper.author ‹bu›}›}, ‹bu›
is indeed a string which refers to a meta-object belonging to the document class typ‹author›, 
for example). With the exception of the @{command "term*"}-command, the term-antiquotations 
 in the other term-contexts are additionally expanded (eg replaced) by the instance of the class,
eg, the HOL-term denoting this meta-object.
This expansion happens ∗‹before› evaluation of the term, thus permitting
executable HOL-functions to interact with meta-objects.
The @{command "assert*"}-command allows for logical statements to be checked in the global context
(see @{technical (unchecked) ‹text_elements_expls›}).
% TODO:
% Section reference @{docitem (unchecked) ‹text_elements_expls›} has not the right number
This is particularly useful to explore formal definitions wrt. their border cases.
For @{command "assert*"}, the evaluation of the term can be disabled
with the boxed_theory_text‹disable_assert_evaluation› theory attribute:
  @{boxed_theory_text [display]‹
  declare[[disable_assert_evaluation]]›}
Then @{command "assert*"} will act like @{command "term*"}.

The @{command "definition*"}-command allows ‹prop›, ‹spec_prems›, and ‹for_fixes›
(see the @{command "definition"} command in cite‹"wenzel:isabelle-isar:2020"›) to contain
term-antiquotations. For example:
@{boxed_theory_text [display]
‹doc_class A =
   level :: "int option"
   x :: int
definition*[a1::A, x=5, level="Some 1"] xx' where "xx' ≡ A.x @{A ‹a1›}" if "A.x @{A ‹a1›} = 5"›}

The @{term_ [source] ‹@{A ‹a1›}›} term-antiquotation is used both in ‹prop› and in ‹spec_prems›.

@{command "lemma*"}, @{command "theorem*"}, etc., are extended versions of the goal commands
defined in cite‹"wenzel:isabelle-isar:2020"›. Term-antiquotations can be used either in
a ‹long_statement› or in a ‹short_statement›.
For instance:
@{boxed_theory_text [display]
‹lemma*[e5::E] testtest : "xx + A.x @{A ‹a1›} = yy + A.x @{A ‹a1›} ⟹ xx = yy"
 by simp›}

This @{command "lemma*"}-command is defined using the @{term_ [source] ‹@{A ‹a1›}›}
term-antiquotation and attaches the @{docitem_name "e5"} instance meta-data to the ‹testtest›-lemma.

@{boxed_theory_text [display]
‹doc_class cc_assumption_test =
a :: int
text*[cc_assumption_test_ref::cc_assumption_test]‹›

definition tag_l :: "'a ⇒ 'b ⇒ 'b" where "tag_l ≡ λx y. y"

lemma* tagged : "tag_l @{cc-assumption-test ‹cc_assumption_test_ref›} AA ⟹ AA"
  by (simp add: tag_l_def)

find_theorems name:tagged "(_::cc_assumption_test ⇒ _ ⇒ _) _ _ ⟹_"›}

In this example, the definition const‹tag_l› adds a tag to the ‹tagged› lemma using
the term-antiquotation @{term_ [source] ‹@{cc_assumption_test ‹cc_assumption_test_ref›}›}
inside the ‹prop› declaration.

Note unspecified attribute values were represented by free fresh variables which constrains dof
to choose either the normalization-by-evaluation strategy ⬚‹nbe› or a proof attempt via
the ⬚‹auto› method. A failure of these strategies will be reported and regarded as non-validation
of this meta-object. The latter leads to a failure of the entire command.
›

(*<*)
declare_reference*["sec_advanced"::technical]
(*>*)

subsection‹Status and Query Commands›

text‹
▪ isadof ‹inspection_command› :
  rail‹    @@{command "print_doc_classes"}
        |  @@{command "print_doc_items"} 
        |  @@{command "check_doc_global"}›
isadof provides a number of inspection commands.
▪ ⬚‹print_doc_classes› allows to view the status of the internal
  class-table resulting from ODL definitions,
▪ ML‹DOF_core.print_doc_class_tree› allows for presenting (fragments) of
  class-inheritance trees (currently only available at ML level),
▪ ⬚‹print_doc_items› allows  to view the status of the internal
  object-table of text-elements that were tracked.
  The theory attribute ⬚‹object_value_debug› allows to inspect
  the term of instances value before its elaboration and normalization.
  Adding:
  @{boxed_theory_text [display]‹
  declare[[object_value_debug = true]]›}
  ... to the theory
  will add the raw value term to the instance object-table for all the subsequent
  declared instances (using ⬚‹text*› for instance).
  The raw term will be available in the ‹input_term› field of ⬚‹print_doc_items› output and,
▪ ⬚‹check_doc_global› checks if all declared object references have been
  defined, all monitors are in a final state, and checks the final invariant  
  on all objects (cf. @{technical (unchecked) ‹sec_advanced›})
›

subsection‹Macros›
text‹
▪ isadof ‹macro_command› :
  rail‹   @@{command "define_shortcut*"} name ('⇌' | '==') '‹' string '›' 
        |  @@{command "define_macro*"}  name ('⇌' | '==') 
           ⏎ '‹' string '›' '_' '‹' string '›' ›

There is a mechanism to define document-local macros which
were PIDE-supported but lead to an expansion in the integrated source; this feature
can be used to define 
▪ ⬚‹shortcuts›, ie, short names that were expanded to, for example,
  LaTeX-code,
▪ ⬚‹macro›'s (= parameterized short-cuts), which allow for 
  passing an argument to the expansion mechanism.
›
text‹The argument can be checked by an own SML-function with respect to syntactic
as well as semantic regards; however, the latter feature is currently only accessible at
the SML level and not directly in the Isar language. We would like to stress, that this 
feature is basically an abstract interface to existing Isabelle functionality in the document 
generation.
›
subsubsection‹Examples›
text‹
▪ common short-cut hiding LaTeX code in the integrated source:
    @{theory_text [display]
      ‹define_shortcut* eg  ⇌ ‹\eg›  (* Latin: "exempli gratia"  meaning  "for example". *)
                      clearpage ⇌ ‹\clearpage{}››}
▪ non-checking macro:
    @{theory_text [display]
      ‹define_macro* index  ⇌ ‹\index{› _ ‹}››}
▪ checking macro:
    @{theory_text [display]
      ‹setup‹ DOF_lib.define_macro binding‹vs›  "\\vspace{" "}" (check_latex_measure) ››}
  where ML‹check_latex_measure› is a hand-programmed function that checks 
  the input for syntactical and static semantic constraints.
›

section‹The Standard Ontology Libraries›
text‹ We will describe the backbone of the Standard Library with the
already mentioned hierarchy ▩‹COL› (the common ontology library),
 ▩‹scholarly_paper› (for MINT-oriented scientific papers) or 
 ▩‹technical_report› (for MINT-oriented technical reports).
›

subsection‹Common Ontology Library (COL)›
(*<*)
ML‹writeln (DOF_core.print_doc_class_tree @{context} (fn (_,l) => String.isPrefix "Isa_COL" l) I)›
(*>*)
text‹ 

 isadof provides a Common Ontology Library (COL)index‹Common Ontology Library!COL@see COL›
 bindex‹COL› ⁋‹contained in theory‹Isabelle_DOF.Isa_COL››
 that introduces several ontology concepts; its  overall class-tree it provides looks as follows:
%
latex‹
\begin{center}
\begin{minipage}{.9\textwidth}\footnotesize
\dirtree{%
.0 .
.1 Isa\_COL.text\_element.
.2 Isa\_COL.chapter.
.2 Isa\_COL.section.
.2 Isa\_COL.subsection.
.2 Isa\_COL.subsubsection.
.1 Isa\_COL.float{...}.
.2 Isa\_COL.figure{...}.
.2 Isa\_COL.listing{...}.
.1 \ldots.
}
\end{minipage}
\end{center}››

text‹
In particular it defines the super-class typ‹text_element›: the root of all 
text-elements:
@{boxed_theory_text [display]‹
doc_class text_element = 
   level         :: "int  option"    <=  "None" 
   referentiable :: bool <= "False"
   variants      :: "String.literal set" <= "{STR ''outline'', STR ''document''}" 
›}

As mentioned in @{scholarly_paper.technical ‹sss›},
const‹level› defines the section-level (eg, using a LaTeX-inspired hierarchy:
from boxed_theory_text‹Some -1› (corresponding to boxed_latex‹\part›) to 
boxed_theory_text‹Some 0› (corresponding to boxed_latex‹\chapter›, respectively, boxed_theory_text‹chapter*›) 
to boxed_theory_text‹Some 3› (corresponding to boxed_latex‹\subsubsection›, respectively, 
boxed_theory_text‹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 requires that technical text section are introduce by a section element).

The attribute const‹referentiable› captures the information if a text-element can be a target
for a reference, which is the case for sections or subsections, for example, but not arbitrary
elements such as, ie, paragraphs (this mirrors restrictions of the target LaTeX representation).
The attribute  const‹variants› refers to an Isabelle-configuration attribute that permits
to steer the different versions of a LaTeX-presentation of the integrated source.

For further information of the root classes such as bindex‹float› typ‹float›'s, please consult 
the ontology in theory‹Isabelle_DOF.Isa_COL› directly and consult the Example I and II for 
their pragmatics. The  theory‹Isabelle_DOF.Isa_COL› also provides  the subclasses
typ‹figure› bindex‹figure› and bindex‹listing› typ‹listing› which together with specific 
text-antiquotations like:
   ▸ ‹@{theory_text [options] "path"}›  (Isabelle)
   ▸ ‹@{fig_content (width=…, height=…, caption=…) "path"}› (COL)
   ▸ ‹@{boxed_theory_text [display] ‹ ... › }› (local, e.g. manual)
   ▸ ‹@{boxed_sml [display] ‹ ... › }› (local, e.g. manual)
   ▸ ‹@{boxed_pdf [display] ‹ ... › }› (local, e.g. manual)
   ▸ ‹@{boxed_latex [display] ‹ ... › }› (local, e.g. manual)
   ▸ ‹@{boxed_bash [display] ‹ ... › }› (local, e.g. manual)›

(*<*)
text‹With these primitives, it is possible to compose listing-like text-elements or 
side-by-side-figures as shown in the subsequent example:
  
@{boxed_theory_text [display]‹
text*[inlinefig::float, 
      main_caption="‹The Caption.›"]
     ‹@{theory_text [display, margin = 5] ‹lemma A :: "a ⟶ b"›}›

text*[dupl_graphics::float, 
      main_caption="‹The Caption.›"]
‹
@{fig_content (width=40, height=35, caption="This is a left test") "figures/A.png"
}hfill@{fig_content (width=40, height=35, caption="This is a right term‹σi + 1› test") "figures/B.png"} 
››}›

text‹The ⬚‹side_by_side_figure*›-command  bindex‹side\_by\_side\_figure› has been deprecated.›
(*>*)

text‹
▩‹COL› finally provides macros that extend the command-language of the DOF core by the following
abbreviations:

▪ ‹derived_text_element› :
rail‹
    (  ( @@{command "chapter*"} 
       | @@{command "section*"}   | @@{command "subsection*"} | @@{command "subsubsection*"} 
       | @@{command "paragraph*"} 
       | @@{command "figure*"}    | @@{command "listing*"} 
       ) 
       ⏎
       '[' meta_args ']' '‹' text '›'
     ) 
  ›
›
text‹The command syntax follows the implicit convention to add a ``*''
to distinguish them from the (similar) standard Isabelle text-commands
which are not ontology-aware.›

subsection*["text_elements"::technical]‹The Ontology ▩‹scholarly_paper››
(*<*)
ML‹val toLaTeX = String.translate (fn c => if c = #"_" then "\\_" else String.implode[c])›     
ML‹writeln (DOF_core.print_doc_class_tree 
                 @{context} (fn (_,l) =>        String.isPrefix "scholarly_paper" l 
                                         orelse String.isPrefix "Isa_COL" l) 
                 toLaTeX)›
(*>*)
text‹ The ▩‹scholarly_paper› ontology is oriented towards the classical domains in science:
mathematics, informatics, natural sciences, technology, or engineering.

It extends ▩‹COL› by the following concepts:
latex‹
\begin{center}
\begin{minipage}{.9\textwidth}\footnotesize
\dirtree{%
.0 .
.1 scholarly\_paper.title.
.1 scholarly\_paper.subtitle.
.1 scholarly\_paper.author\DTcomment{An Author Entity Declaration}.
.1 scholarly\_paper.abstract.
.1 Isa\_COL.text\_element.
.2 scholarly\_paper.text\_section\DTcomment{Major Paper Text-Elements}.    
.3 scholarly\_paper.introduction\DTcomment{...}.
.3 scholarly\_paper.conclusion\DTcomment{...}.
.4 scholarly\_paper.related\_work\DTcomment{...}.
.3 scholarly\_paper.bibliography\DTcomment{...}.
.3 scholarly\_paper.annex\DTcomment{...}.
.3 scholarly\_paper.example\DTcomment{Example in General Sense}.
.3 scholarly\_paper.technical\DTcomment{Root for Technical Content}.
.4 scholarly\_paper.math\_content\DTcomment{...}.
.5 scholarly\_paper.definition\DTcomment{Freeform}.
.5 scholarly\_paper.lemma\DTcomment{Freeform}.
.5 scholarly\_paper.theorem\DTcomment{Freeform}.
.5 scholarly\_paper.corollary\DTcomment{Freeform}.
.5 scholarly\_paper.math\_example\DTcomment{Freeform}.
.5 scholarly\_paper.math\_semiformal\DTcomment{Freeform}.
.5 scholarly\_paper.math\_formal\DTcomment{Formal Content}.
.6 scholarly\_paper.assertion\DTcomment{Assertions}.
.4 scholarly\_paper.tech\_example\DTcomment{...}.
.4 scholarly\_paper.math\_motivation\DTcomment{...}.
.4 scholarly\_paper.math\_explanation\DTcomment{...}.
.4 scholarly\_paper.engineering\_content\DTcomment{...}.
.5 scholarly\_paper.data.
.5 scholarly\_paper.evaluation.
.5 scholarly\_paper.experiment.
.4 ... 
.1 ... 
.1 scholarly\_paper.article\DTcomment{The Paper Monitor}.
.1 \ldots.
}
\end{minipage}
\end{center}
››


text‹Recall that ∗‹Formal Content› means ∗‹machine-checked, validated content›.›

text‹A pivotal abstract class in the hierarchy is:
@{boxed_theory_text [display]
‹
doc_class text_section = text_element +
   main_author :: "author option"  <=  None
   fixme_list  :: "string list"    <=  "[]" 
   level       :: "int  option"    <=  "None"  
›}

Besides attributes of more practical considerations like a const‹fixme_list›, that can be modified
during the editing process but is only visible in the integrated source but usually ignored in the
LaTeX, this class also introduces the possibility to assign an ``ownership'' or ``responsibility'' of 
a typ‹text_element› to a specific typ‹author›. Note that this is possible since isadof assigns to each
document class also a class-type which is declared in the HOL environment.›

text*[s23::example, main_author = "Some(@{scholarly_paper.author ‹bu›})"]‹
Recall that concrete authors can be denoted by term-antiquotations generated by isadof; for example,
this may be for a text fragment like
@{boxed_theory_text [display]
‹text*[…::example, main_author = "Some(@{author ''bu''})"] ‹ … ››}
or 
@{boxed_theory_text [display]
‹text*[…::example, main_author = "Some(@{author ‹bu›})"] ‹ … ››}

where boxed_theory_text‹"''bu''"› is a string presentation of the reference to the author 
text element (see below in @{docitem (unchecked) ‹text_elements_expls›}).
% TODO:
% Section reference @{docitem (unchecked) ‹text_elements_expls›} has not the right number
›

text‹Some of these concepts were supported as command-abbreviations leading to the extension
of the isadof language:

▪ ‹derived_text_elements › :
rail‹
    (  ( @@{command "author*"}     | @@{command "abstract*"} 
       | @@{command "Definition*"} | @@{command "Lemma*"}      | @@{command "Theorem*"} 
       | @@{command "Proposition*"}| @@{command "Proof*"}      | @@{command "Example*"}  
       | @@{command "Premise*"}    | @@{command "Assumption*"} | @@{command "Hypothesis*"}
       | @@{command "Corollary*"}  | @@{command "Consequence*"}| @@{command "Assertion*"}
       | @@{command "Conclusion*"} 
       ) 
       ⏎
       '[' meta_args ']' '‹' text '›'
     ) 
     
  ›
›




text‹Usually, command macros for text elements will assign the generated instance
to the default class corresponding for this class.
For pragmatic reasons, ⬚‹Definition*›,  ⬚‹Lemma*› and  ⬚‹Theorem*› represent an exception
to this rule and are set up such that the default class is the super class @{typ ‹math_content›}
(rather than to the class @{typ ‹definition›}).
This way, it is possible to use these macros for several  sorts of the very generic
concept ``definition'', which can be used as a freeform mathematical definition but also for a
freeform terminological definition as used in certification standards. Moreover, new subclasses
of @{typ ‹math_content›} might be introduced in a derived ontology with an own specific layout
definition. 
›

text‹While this library is intended to give a lot of space to freeform text elements in
order to counterbalance Isabelle's standard view, it should not be forgotten that the real strength
of Isabelle is its ability to handle both, and to establish links between both worlds. 
Therefore, the formal assertion command has been integrated to capture some form of formal content.›


subsubsection*["text_elements_expls"::example]‹Examples›

text‹
  While the default user interface for class definitions via the  
  boxed_theory_text‹text*‹ ... ››-command allow to access all features of the document 
  class, isadof provides short-hands for certain, widely-used, concepts such as 
  boxed_theory_text‹title*‹ ... ›› or boxed_theory_text‹section*‹ ... ››, eg:

@{boxed_theory_text [display]‹
title*[title::title]‹Isabelle/DOF›
subtitle*[subtitle::subtitle]‹User and Implementation Manual›
author*[adb::author, email="‹a.brucker@exeter.ac.uk›",
        orcid="‹0000-0002-6355-1200›", http_site="‹https://brucker.ch/›",
        affiliation="‹University of Exeter, Exeter, UK›"] ‹Achim D. Brucker›
author*[bu::author, email = "‹wolff@lri.fr›",
         affiliation = "‹Université Paris-Saclay, LRI, Paris, France›"]‹Burkhart Wolff››}

›

text‹Assertions allow for logical statements to be checked in the global context.
This is particularly useful to explore formal definitions wrt. their border cases.
@{boxed_theory_text [display]‹
assert*[ass1::assertion, short_name = "‹This is an assertion›"] ‹last [3] < (4::int)››}
›

text‹We want to check the consequences of this definition and can add the following statements:
@{boxed_theory_text [display]‹
text*[claim::assertion]‹For non-empty lists, our definition yields indeed 
                               the last element of a list.›
assert*[claim1::assertion] ‹last[4::int] = 4›    
assert*[claim2::assertion] ‹last[1,2,3,4::int] = 4››}
›

text‹
As mentioned before, the command macros of  ⬚‹Definition*›,  ⬚‹Lemma*› and  ⬚‹Theorem*› 
set the default class to the super-class of typ‹definition›.
However, in order to avoid the somewhat tedious consequence:
@{boxed_theory_text [display]
‹Theorem*[T1::"theorem", short_name="‹DF definition captures deadlock-freeness›"]  ‹ … ››}

the choice of the default class can be influenced by setting globally an attribute such as
@{boxed_theory_text [display]
‹declare[[Definition_default_class = "definition"]]
declare[[Theorem_default_class = "theorem"]]›}

which allows the above example be shortened to:
@{boxed_theory_text [display]
‹Theorem*[T1, short_name="‹DF definition captures deadlock-freeness›"]  ‹ … ››}
›

subsection‹The Ontology ▩‹technical_report››
(*<*)
ML‹val toLaTeX = String.translate (fn c => if c = #"_" then "\\_" else String.implode[c])›     
ML‹writeln (DOF_core.print_doc_class_tree 
                 @{context} (fn (_,_) =>  true (*     String.isPrefix "technical_report" l 
                                         orelse String.isPrefix "Isa_COL" l *)) 
                 toLaTeX)›
(*>*)
text‹ The ▩‹technical_report› bindex‹technical\_report› ontology in
 theory‹Isabelle_DOF.technical_report› extends
▩‹scholarly_paper›  bindex‹scholarly\_paper› bindex‹ontology› by concepts needed 
for larger reports in the domain of mathematics and engineering. The concepts are fairly 
high-level arranged at root-class level,

%
latex‹
\begin{center}
\begin{minipage}{.9\textwidth}\footnotesize
\dirtree{%
.0 .
.1 technical\_report.front\_matter\DTcomment{...}.
.1 technical\_report.table\_of\_contents\DTcomment{...}.
.1 Isa\_COL.text\_element\DTcomment{...}.
.2 scholarly\_paper.text\_section\DTcomment{...}.
.4 technical\_report.code\DTcomment{...}.
.5 technical\_report.SML\DTcomment{...}.
.5 technical\_report.ISAR\DTcomment{...}.
.5 technical\_report.LATEX\DTcomment{...}.
.1 technical\_report.index\DTcomment{...}.
.1 ... 
.1 technical\_report.report\DTcomment{...}.
}
\end{minipage}
\end{center}
››




subsubsection‹For Isabelle Hackers: Defining New Top-Level Commands›

text‹
  Defining such new top-level commands requires some Isabelle knowledge as well as 
  extending the dispatcher of the LaTeX-backend. For the details of defining top-level 
  commands, we refer the reader to the Isar manual~cite‹"wenzel:isabelle-isar:2020"›. 
  Here, we only give a brief example how the boxed_theory_text‹section*›-command is defined; we 
  refer the reader to the source code of isadof for details.

  First, new top-level keywords need to be declared in the boxed_theory_text‹keywords›-section of 
  the theory header defining new keywords:

@{boxed_theory_text [display]‹
theory 
    ...
  imports
    ... 
  keywords
    "section*"
begin 
...
end
›}

Second, given an implementation of the functionality of the new keyword (implemented in SML), 
the new keyword needs to be registered, together with its parser, as outer syntax:
latex‹
\begin{sml}
val _ =
  Outer_Syntax.command ("section*", <@>{here}) "section heading"
    (attributes -- Parse.opt_target -- Parse.document_source --| semi
      >> (Toplevel.theory o (enriched_document_command (SOME(SOME 1)) 
           {markdown = false} )));
\end{sml}›
›

text‹
Finally, for the document generation, a new dispatcher has to be defined in LaTeX---this is 
mandatory, otherwise the document generation will break. These dispatchers always follow the same 
schemata:
latex‹
\begin{ltx}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% begin: section*-dispatcher
\NewEnviron{isamarkupsection*}[1][]{\isaDof[env={section},#1]{\BODY}}
% end: section*-dispatcher
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\end{ltx}
›
  After the definition of the dispatcher, one can, optionally, define a custom representation 
  using the boxed_latex‹\newisadof›-command, as introduced in the previous section: 
latex‹
\begin{ltx}
\newisadof{section}[label=,type=][1]{%
  \isamarkupfalse%
    \isamarkupsection{#1}\label{\commandkey{label}}%
  \isamarkuptrue%
}
\end{ltx}›
›



section*["sec_advanced"::technical]‹Advanced ODL Concepts›
(*<*)
doc_class title =
  short_title :: "string option" <= "None"
doc_class author =
  email :: "string" <= "''''"
datatype classification = SIL0 | SIL1 | SIL2 | SIL3 | SIL4
doc_class abstract =
  keywordlist :: "string list" <= "[]"
  safety_level :: "classification" <= "SIL3"
doc_class text_section =
  authored_by :: "author set" <= "{}"
  level :: "int option" <= "None"
type_synonym notion = string
doc_class introduction = text_section +
  authored_by :: "author set"  <= "UNIV"
  uses :: "notion set"
doc_class claim = introduction +
  based_on :: "notion list"
doc_class technical = text_section +
  formal_results :: "thm list"
doc_class "definition" = technical +
  is_formal :: "bool"
  property  :: "term list" <= "[]"
datatype kind = expert_opinion | argument | "proof"
doc_class result = technical +
  evidence :: kind
  property :: "thm list" <= "[]"
doc_class example = technical +
  referring_to :: "(notion + definition) set" <= "{}"
doc_class "conclusion" = text_section +
  establish :: "(claim × result) set"
(*>*)

subsection*["sec_example"::technical]‹Example›
text‹We assume in this section the following local ontology: 

@{boxed_theory_text [display]‹
doc_class title =
  short_title :: "string option" <= "None"
doc_class author =
  email :: "string" <= "''''"
datatype classification = SIL0 | SIL1 | SIL2 | SIL3 | SIL4
doc_class abstract =
  keywordlist :: "string list" <= "[]"
  safety_level :: "classification" <= "SIL3"
doc_class text_section =
  authored_by :: "author set" <= "{}"
  level :: "int option" <= "None"
type_synonym notion = string
doc_class introduction = text_section +
  authored_by :: "author set"  <= "UNIV" 
  uses :: "notion set"
doc_class claim = introduction +
  based_on :: "notion list" 
doc_class technical = text_section +
  formal_results :: "thm list" 
doc_class "definition" = technical +
  is_formal :: "bool"
  property  :: "term list" <= "[]" 
datatype kind = expert_opinion | argument | "proof"
doc_class result = technical +
  evidence :: kind
  property :: "thm list" <= "[]"
doc_class example = technical +
  referring_to :: "(notion + definition) set" <= "{}"
doc_class "conclusion" = text_section +
  establish :: "(claim × result) set"
›}
›

subsection‹Meta-types as Types›
(* TODO: Update the previous example and this section by importing an ontology
   and using checking antiquotations like const ans typ *)
text‹
  To express the dependencies between text elements to the formal
  entities, eg, ML_type‹term› (‹λ›-term), ML_type‹typ›, or
   ML_type‹thm›, we represent the types of the implementation language
  ∗‹inside› the HOL type system.  We do, however, not reflect the data of
  these types. They are just types declared in HOL, 
  which are ``inhabited'' by special constant symbols carrying strings, for
  example of the format boxed_theory_text‹@{thm <string>}›.
  When HOL
  expressions were used to denote values of boxed_theory_text‹doc_class›
  instance attributes, this requires additional checks after
  conventional type-checking that this string represents actually a
  defined entity in the context of the system state
  boxed_theory_text‹θ›.  For example, the boxed_theory_text‹establish›
  attribute in our example is the power of the ODL: here, we model
  a relation between ∗‹claims› and ∗‹results› which may be a
  formal, machine-check theorem of type ML_type‹thm› denoted by, for
  example: boxed_theory_text‹property = "[@{thm "system_is_safe"}]"› in a
  system context boxed_theory_text‹θ› where this theorem is
  established. Similarly, attribute values like 
  boxed_theory_text‹property = "@{term ‹A ⟷ B›}"›
  require that the HOL-string boxed_theory_text‹A ⟷ B› is 
  again type-checked and represents indeed a formula in ‹θ›. Another instance of 
  this process, which we call ∗‹second-level type-checking›, are term-constants
  generated from the ontology such as 
  boxed_theory_text‹@{definition <string>}›. 
›

(*<*)
declare_reference*["sec_monitors"::technical]
declare_reference*["sec_low_level_inv"::technical]
(*>*)

subsection*["sec_class_inv"::technical]‹ODL Class Invariants›

text‹
  Ontological classes as described so far are too liberal in many situations.
  There is a first high-level syntax implementation for class invariants.
  These invariants are checked when an instance of the class is defined,
  and trigger warnings.
  The checking is enabled by default but can be disabled with the
  boxed_theory_text‹invariants_checking› theory attribute:
  @{boxed_theory_text [display]‹
  declare[[invariants_checking = false]]›}

  To enable the strict checking of the invariants,
  that is to trigger errors instead of warnings,
  the boxed_theory_text‹invariants_strict_checking›
  theory attribute must be set:
  @{boxed_theory_text [display]‹
  declare[[invariants_strict_checking = true]]›}

  For example, let's define the following two classes:
  @{boxed_theory_text [display]‹
  doc_class class_inv1 =
    int1 :: "int"
    invariant inv1 :: "int1 σ ≥ 3"

  doc_class class_inv2 = class_inv1 +
    int2 :: "int"
    invariant inv2 :: "int2 σ < 2"
  ›}

  The boxed_theory_text‹σ› symbol is reserved and references the future instance class.
  By relying on the implementation of the Records
  in Isabelle/HOL~cite‹"wenzel:isabelle-isar:2020"›,
  one can reference an attribute of an instance using its selector function.
  For example, boxed_theory_text‹int1 σ› denotes the value
  of the boxed_theory_text‹int1› attribute
  of the future instance of the class boxed_theory_text‹class_inv1›.

  Now let's define two instances, one of each class:

  @{boxed_theory_text [display]‹
  text*[testinv1::class_inv1, int1=4]‹lorem ipsum...›
  text*[testinv2::class_inv2, int1=3, int2=1]‹lorem ipsum...›
  ›}

  The value of each attribute defined for the instances is checked against their classes invariants.
  As the class boxed_theory_text‹class_inv2› is a subsclass
  of the class boxed_theory_text‹class_inv1›, it inherits boxed_theory_text‹class_inv1› invariants.
  Hence, the boxed_theory_text‹inv1› invariant is checked
  when the instance boxed_theory_text‹testinv2› is defined.

  Now let's add some invariants to our example in technical‹sec_example›.
  For example, one
  would like to express that any instance of a boxed_theory_text‹result› class finally has
  a non-empty  property list, if its boxed_theory_text‹kind› is boxed_theory_text‹proof›, or that 
  the boxed_theory_text‹establish› relation between boxed_theory_text‹claim› and
  boxed_theory_text‹result› is total.
  In a high-level syntax, this type of constraints could be expressed, eg, by:
  @{boxed_theory_text [display]‹
  doc_class introduction = text_section +
    authored_by :: "author set"  <= "UNIV" 
    uses :: "notion set"
    invariant author_finite :: "finite (authored_by σ)"
  doc_class result = technical +
    evidence :: kind
    property :: "thm list" <= "[]"
    invariant has_property :: "evidence σ = proof ⟷ property σ ≠ []"
  doc_class example = technical +
    referring_to :: "(notion + definition) set" <= "{}"
  doc_class conclusion = text_section +
    establish :: "(claim × result) set"
    invariant total_rel :: "∀ x. x ∈ Domain (establish σ)
                                             ⟶ (∃ y ∈ Range (establish σ). (x, y) ∈ establish σ)"
  ›}
  All specified constraints are already checked in the IDE of dof while editing.
  The invariant boxed_theory_text‹author_finite› enforces that the user sets the 
  boxed_theory_text‹authored_by› set.
  The invariants ⬚‹author_finite› and ⬚‹establish_defined› can not be checked directly
  and need a little help.
  We can set the ‹invariants_checking_with_tactics› theory attribute to help the checking.
  It will enable a basic tactic, using unfold and auto:
  @{boxed_theory_text [display]‹
  declare[[invariants_checking_with_tactics = true]]›}
  There are still some limitations with this high-level syntax.
  For now, the high-level syntax does not support the checking of
  specific monitor behaviors (see @{technical (unchecked) "sec_monitors"}).
  For example, one would like to delay a final error message till the
  closing of a monitor.
  For this use-case you can use low-level class invariants
  (see @{technical (unchecked) "sec_low_level_inv"}).
  Also, for now, term-antiquotations can not be used in an invariant formula.
›


subsection*["sec_low_level_inv"::technical]‹ODL Low-level Class Invariants›

text‹
  If one want to go over the limitations of the actual high-level syntax of the invariant,
  one can define a function using SML.
  A formulation, in SML, of the class-invariant boxed_theory_text‹has_property›
  in technical‹sec_class_inv›, defined in the supposedly ‹Low_Level_Syntax_Invariants› theory
  (note the long name of the class),
  is straight-forward:

@{boxed_sml [display]
‹fun check_result_inv oid {is_monitor:bool} ctxt =
  let
    val kind =
      ISA_core.compute_attr_access ctxt "evidence" oid NONE @{here}
    val prop =
      ISA_core.compute_attr_access ctxt "property" oid NONE @{here}
    val tS = HOLogic.dest_list prop
  in  case kind of
       @{term "proof"} => if not(null tS) then true
                          else error("class result invariant violation")
      | _ => true
  end
val cid_long = DOF_core.get_onto_class_name_global "result" @{theory}
val bind = Binding.name "Check_Result"
val _ = Theory.setup (DOF_core.make_ml_invariant (check_result_inv, cid_long)
                     |> DOF_core.add_ml_invariant bind)›}

  The ML‹Theory.setup›-command (last line) registers the boxed_theory_text‹check_result_inv› function 
  into the isadof kernel, which activates any creation or modification of an instance of 
  boxed_theory_text‹result›. We cannot replace boxed_theory_text‹compute_attr_access› by the 
  corresponding antiquotation boxed_theory_text‹value_‹evidence @{result ‹oid›}››, since
  boxed_theory_text‹oid› is bound to a  variable here and can therefore not be statically expanded.
›

subsection*["sec_monitors"::technical]‹ODL Monitors›
text‹
  We call a document class with an ‹accepts_clause› a ∗‹monitor›.bindex‹monitor›  Syntactically, an 
  ‹accepts_clause›index‹accepts\_clause@‹accepts_clause›› contains a regular expression over class identifiers. 
  For example:

  @{boxed_theory_text [display]‹
  doc_class article = 
     style_id :: string                <= "''LNCS''"
     version  :: "(int × int × int)"  <= "(0,0,0)"
     accepts "(title ~~ ⟦subtitle⟧ ~~ ⦃author⦄+ ~~ abstract ~~ ⦃introduction⦄+
                   ~~ ⦃background⦄* ~~ ⦃technical || example ⦄+ ~~ ⦃conclusion⦄+
                   ~~ bibliography ~~ ⦃annex⦄* )"
  ›}

  Semantically, monitors introduce a behavioral element into ODL:

  @{boxed_theory_text [display]‹
  open_monitor*[this::article]  (* begin of scope of monitor "this" *)
    ...
  close_monitor*[this]          (* end of scope of monitor "this"   *)
  ›}

  Inside the scope of a monitor, all instances of classes mentioned in its ▩‹accepts_clause› (the
  ∗‹accept-set›) have to appear in the order specified by the regular expression; instances not 
  covered by an accept-set may freely occur. Monitors may additionally contain a ▩‹rejects_clause› 
  with a list of class-ids (the reject-list). This allows specifying ranges of
  admissible instances along the class hierarchy:
  ▪ a superclass in the reject-list and a subclass in the
    accept-expression forbids instances superior to the subclass, and
  ▪ a subclass $S$ in the reject-list and a superclass ‹T› in the
    accept-list allows instances of superclasses of ‹T› to occur freely,
    instances of ‹T› to occur in the specified order and forbids
    instances of ‹S›.
›
text‹
  Should the specified ranges of admissible instances not be observed, warnings will be triggered.
  To forbid the violation of the specified ranges,
  one can enable the boxed_theory_text‹strict_monitor_checking› theory attribute:
  @{boxed_theory_text [display]‹declare[[strict_monitor_checking = true]]›}
  It is possible to enable the tracing of free classes occurring inside the scope of a monitor by
  enabling the boxed_theory_text‹free_class_in_monitor_checking›
  theory attribute:
  @{boxed_theory_text [display]‹declare[[free_class_in_monitor_checking = true]]›}
  Then a warning will be triggered when defining an instance of a free class
  inside the scope of a monitor.
  To forbid free classes inside the scope of a monitor, one can enable the
  boxed_theory_text‹free_class_in_monitor_strict_checking› theory attribute:
  @{boxed_theory_text [display]‹declare[[free_class_in_monitor_strict_checking = true]]›}

  Monitored document sections can be nested and overlap; thus, it is
  possible to combine the effect of different monitors. For example, it
  would be possible to refine the boxed_theory_text‹example› section by its own
  monitor and enforce a particular structure in the presentation of
  examples.
  
  Monitors manage an implicit attribute boxed_theory_text‹trace› containing
  the list of ``observed'' text element instances belonging to the
  accept-set. Together with the concept of ODL class invariants, it is
  possible to specify properties of a sequence of instances occurring in
  the document section. For example, it is possible to express that in
  the sub-list of boxed_theory_text‹introduction›-elements, the first has an
  boxed_theory_text‹introduction› element with a boxed_theory_text‹level› strictly
  smaller than the others. Thus, an introduction is forced to have a
  header delimiting the borders of its representation. Class invariants
  on monitors allow for specifying structural properties on document
  sections.
  For now, the high-level syntax of invariants does not support the checking of
  specific monitor behaviors like the one just described and you must use 
  the low-level class invariants (see @{technical "sec_low_level_inv"}).

  Low-level invariants checking can be set up to be triggered
  when opening a monitor, when closing a monitor, or both
  by using the ML‹DOF_core.add_opening_ml_invariant›,
  ML‹DOF_core.add_closing_ml_invariant›, or ML‹DOF_core.add_ml_invariant› commands
  respectively, to add the invariants to the theory context
  (See @{technical "sec_low_level_inv"} for an example).
›

(*<*)
value*‹map (result.property) @{instances_of ‹result›}›
value*‹map (text_section.authored_by) @{instances_of ‹introduction›}›
value*‹filter (λσ. result.evidence σ = proof) @{instances_of ‹result›}›
value*‹filter (λσ. the (text_section.level σ) > 1) @{instances_of ‹introduction›}›
(*>*)

subsection*["sec_queries_on_instances"::technical]‹Queries On Instances›

text‹
  Any class definition generates term antiquotations checking a class instance or
  the set of instances in a particular logical context; these references were
  elaborated to objects they refer to.
  This paves the way for a new mechanism to query the ``current'' instances presented as a
  HOL type‹list›.
  Arbitrarily complex queries can therefore be defined inside the logical language.
  To get the list of the properties of the instances of the class ‹result›,
  or to get the list of the authors of the instances of ‹introduction›,
  it suffices to treat this meta-data as usual:
  @{theory_text [display,indent=5, margin=70] ‹
value*‹map (result.property) @{instances_of ‹result›}›
value*‹map (text_section.authored_by) @{instances_of ‹introduction›}›
  ›}
  In order to get the list of the instances of the class ‹myresult›
  whose ‹evidence› is a ‹proof›, one can use the command:
  @{theory_text [display,indent=5, margin=70] ‹
value*‹filter (λσ. result.evidence σ = proof) @{instances_of ‹result›}›
  ›}
  The list of the instances of the class ‹introduction› whose ‹level› > 1,
  can be filtered by:
  @{theory_text [display,indent=5, margin=70] ‹
value*‹filter (λσ. the (text_section.level σ) > 1) @{instances_of ‹introduction›}›
  ›}
›

section*[infrastructure::technical]‹Technical Infrastructure›

subsection‹The Previewer›

figure*[ 
  global_DOF_view::figure
  , relative_width="95" 
  , file_src="''figures/ThisPaperWithPreviewer.png''" 
]‹A Screenshot while editing this Paper in dof with Preview.›
text‹A screenshot of the editing environment is shown in figure‹global_DOF_view›. It supports 
incremental continuous PDF generation which  improves  usability. Currently, the granularity 
is restricted to entire theories (which have to be selected in a specific document pane). 
The response times can not (yet) compete
with a Word- or Overleaf editor, though, which is mostly due to the checking and 
evaluation overhead (the turnaround of this section is about 30 s). However, we believe
that better parallelization and evaluation techniques will decrease this gap substantially for the 
most common cases in future versions. ›


subsection‹Developing Ontologies and their Representation Mappings›
text‹
  The document core ∗‹may›, but ∗‹must› not use Isabelle definitions or proofs for checking the 
  formal content---this manual is actually an example of a document not containing any proof.
  Consequently, the document editing and checking facility provided by isadof addresses the needs 
  of common users for an advanced text-editing environment, neither modeling nor proof knowledge is 
  inherently required.

  We expect authors of ontologies to have experience in the use of isadof, basic modeling (and, 
  potentially, some basic SML programming) experience, basic LaTeX knowledge, and, last but not 
  least, domain knowledge of the ontology to be modeled. Users with experience in UML-like 
  meta-modeling will feel familiar with most concepts; however, we expect  no need for insight in 
  the Isabelle proof language, for example, or other more advanced concepts.

  Technically, ontologiesindex‹ontology!directory structure› are stored in a directory 
  boxed_bash‹ontologies› and consist of an Isabelle theory file and a LaTeX-style file:
%
latex‹
\begin{center}
\begin{minipage}{.9\textwidth}\footnotesize
\dirtree{%
.1 .
.2 ontologies\DTcomment{Ontologies}.
.3 ontologies.thy\DTcomment{Ontology Registration}.
.3 scholarly\_paper\DTcomment{scholarly\_paper}.
.4 scholarly\_paper.thy.
.4 DOF-scholarly\_paper.sty.
.3 technical\_report\DTcomment{technical\_paper}.
.4 technical\_report.thy.
.4 DOF-technical\_report.sty.
}
\end{minipage}
\end{center}›
›
text‹
  Developing a new ontology ``boxed_bash‹foo›'' requires the 
  following steps:
  ▪ definition of the ontological concepts, using isadof's Ontology Definition Language (ODL), in 
    a new theory file path‹ontologies/foo/foo.thy›.  
  ▪ definition of the document representation for the ontological concepts in a \LaTeX-style 
    stored in the same directory as the theory file containing the ODL definitions. The file name should 
    start with the prefix ``DOF-``. For instance: path‹DOF-foo.sty›
  ▪ registration of the \LaTeX-style by adding a suitable ⬚‹define_ontology› 
    command to the theory containing the ODL definitions.
›

subsection‹Document Templates›
text‹
  Document-templatesindex‹document template› define the overall layout (page size, margins, fonts, 
  etc.) of the generated documents. Document-templates 
  are stored in a directory 
  path‹src/document-templates›:index‹document template!directory structure›
latex‹
\begin{center}
\begin{minipage}{.9\textwidth}\footnotesize
\dirtree{%
.1 .
.2 document-templates\DTcomment{Document templates}.
.3 root-lncs.tex.
.3 root-scrartcl.tex.
.3 root-scrreprt-modern.tex.
.3 root-scrreprt.tex.
}
\end{minipage}
\end{center}›
›

text‹
  Developing a new document template ``boxed_bash‹bar›'' requires the following steps:
  ▪ develop a new LaTeX-template boxed_bash‹src/document-templates/root-bar.tex›
  ▪ add a suitable ⬚‹define_template› command to a theory that is 
   imported by the project that shall use the new document template. 
›


text‹
  As the document generation of isadof is based on LaTeX, the isadof document templates can (and 
  should) make use of any LaTeX-classes provided by publishers or standardization bodies.
›


section*["document_templates"::technical]‹Defining Document Templates›
subsection‹The Core Template›

text‹
  Document-templatesbindex‹document template› define the overall layout (page size, margins, fonts, 
  etc.) of the generated documents.
  If a new layout is already supported by a LaTeX-class, then developing basic support for it 
  is straightforward: In most cases, it is 
  sufficient to replace the document class in \autoref{lst:dc} of the template and add the 
  LaTeX-packages that are (strictly) required by the used LaTeX-setup. In general, we recommend
  to only add LaTeX-packages that are always necessary for this particular template, as loading
  packages in the templates minimizes the freedom users have by adapting the path‹preample.tex›.
  The file name of the new template should start with the prefix path‹root-› and need to be 
  registered using the ⬚‹define_template› command.
  a typical isadof document template looks as follows: 

latex‹
\begin{ltx}[escapechar=ë, numbers=left,numberstyle=\tiny,xleftmargin=5mm]
\documentclass{article}        % The LaTeX-class of your template ë\label{lst:dc}ë  
\usepackage{DOF-core}
\usepackage{subcaption}
\usepackage[size=footnotesize]{caption}
\usepackage{hyperref}

%% Main document, do not modify
\begin{document}
\maketitle
\IfFileExists{dof_session.tex}{\input{dof_session}}{\input{session}}
\IfFileExists{root.bib}{\bibliography{root}}{}
\end{document}
\end{ltx}›
›

subsection‹Tips, Tricks, and Known Limitations›
text‹
  In this section, we will discuss several tips and tricks for developing 
  new or adapting existing document templates or LaTeX-representations of ontologies.
›

subsubsection‹Getting Started›
text‹
  In general, we recommend creating a test project (eg, using boxed_bash‹isabelle dof_mkroot›)
  to develop new document templates or ontology representations. The default setup of the isadof
  build system generated a path‹output/document› directory with a self-contained LaTeX-setup. In 
  this directory, you can directly use LaTeX on the main file, called path‹root.tex›:
  @{boxed_bash [display] ‹ë\prompt{MyProject/output/document}ë lualatex root.tex›}

  This allows you to develop and check your LaTeX-setup without the overhead of running 
   boxed_bash‹isabelle build› after each change of your template (or ontology-style). Note that 
  the content of the path‹output› directory is overwritten by executing 
   boxed_bash‹isabelle build›.
›

subsubsection‹Truncated Warning and Error Messages›
text‹
  By default, LaTeX cuts of many warning or error messages after 79 characters. Due to the 
  use of full-qualified names in isadof, this can often result in important information being 
  cut off. Thus, it can be very helpful to configure LaTeX in such a way that it prints 
  long error or warning messages. This can easily be done for individual 
  LaTeX invocations: 
  @{boxed_bash [display] ‹ë\prompt{MyProject/output/document}ë max_print_line=200 error_line=200 half_error_line=100  lualatex root.tex›}
›

subsubsection‹Deferred Declaration of Information›
text‹
  During document generation, sometimes, information needs to be printed prior to its 
  declaration in a isadof theory. This violation of the declaration-before-use-principle
  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, 
  this is a standard process (eg, used for updating references), implementing it correctly
  requires a solid understanding of LaTeX's expansion mechanism. 
  Examples of this can be found, eg, in the ontology-style 
  🗏‹../../ontologies/scholarly_paper/DOF-scholarly_paper.sty›.
  For details about the expansion mechanism
  in general, we refer the reader to the LaTeX literature (eg,~cite‹"knuth:texbook:1986"
  and "mittelbach.ea:latex:1999" and "eijkhout:latex-cs:2012"›).  
›


subsubsection‹Authors and Affiliation Information›
text‹
  In the context of academic papers, the defining of the representations for the author and
  affiliation information is particularly challenging as, firstly, they inherently are breaking
  the declare-before-use-principle and, secondly, each publisher uses a different LaTeX-setup 
  for their declaration. Moreover, the mapping from the ontological modeling to the document
  representation might also need to bridge the gap between different common modeling styles of 
  authors and their affiliations, namely: affiliations as attributes of authors vs. authors and 
  affiliations both as entities with a many-to-many relationship.

  The ontology representation
  🗏‹../../ontologies/scholarly_paper/DOF-scholarly_paper.sty› contains an example that, firstly, 
  shows how to write the author and affiliation information into the auxiliary file for re-use 
  in the next LaTeX-run and, secondly, shows how to collect the author and affiliation 
  information into an boxed_latex‹\author› and a boxed_latex‹\institution› statement, each of 
  which containing the information for all authors. The collection of the author information 
  is provided by the following LaTeX-code:
latex‹
\begin{ltx}
\def\dof@author{}%
\newcommand{\DOFauthor}{\author{\dof@author}}
\AtBeginDocument{\DOFauthor}
\def\leftadd#1#2{\expandafter\leftaddaux\expandafter{#1}{#2}{#1}}
\def\leftaddaux#1#2#3{\gdef#3{#1#2}}
\newcounter{dof@cnt@author}
\newcommand{\addauthor}[1]{%
  \ifthenelse{\equal{\dof@author}{}}{%
    \gdef\dof@author{#1}%
  }{%
    \leftadd\dof@author{\protect\and #1}%
  }
}
\end{ltx}›

The new command boxed_latex‹\addauthor› and a similarly defined command boxed_latex‹\addaffiliation›
can now be used in the definition of the representation of the concept 
boxed_theory_text‹text.scholarly_paper.author›, which writes the collected information in the 
job's aux-file. The intermediate step of writing this information into the job's aux-file is necessary,
as the author and affiliation information is required right at the beginning of the document 
while  isadof allows defining  authors at  any place within a document:

latex‹
\begin{ltx}
\provideisadof{text.scholarly_paper.author}%
[label=,type=%
,scholarly_paper.author.email=%
,scholarly_paper.author.affiliation=%
,scholarly_paper.author.orcid=%
,scholarly_paper.author.http_site=%
][1]{%
  \stepcounter{dof@cnt@author}
  \def\dof@a{\commandkey{scholarly_paper.author.affiliation}}
  \ifthenelse{\equal{\commandkey{scholarly_paper.author.orcid}}{}}{%
    \immediate\write\@auxout%
       {\noexpand\addauthor{#1\noexpand\inst{\thedof@cnt@author}}}%
  }{%
    \immediate\write\@auxout%
        {\noexpand\addauthor{#1\noexpand%
            \inst{\thedof@cnt@author}%
                 \orcidID{\commandkey{scholarly_paper.author.orcid}}}}%
  }
  \protected@write\@auxout{}{%
               \string\addaffiliation{\dof@a\\\string\email{%
                    \commandkey{scholarly_paper.author.email}}}}%
}
\end{ltx}›

Finally, the collected information is used in the  boxed_latex‹\author› command using the 
boxed_latex‹AtBeginDocument›-hook:
latex‹
\begin{ltx}
\newcommand{\DOFauthor}{\author{\dof@author}}
\AtBeginDocument{%
  \DOFauthor
}

\end{ltx}›

›

subsubsection‹Restricting the Use of Ontologies to Specific Templates›

text‹
  As ontology representations might rely on features only provided by certain templates 
  (LaTeX-classes), authors of ontology representations might restrict their use to 
  specific classes. This can, eg, be done using the ltxinline‹\@ifclassloaded{}› command:
latex‹
\begin{ltx}
\@ifclassloaded{llncs}{}%
{% LLNCS class not loaded
    \PackageError{DOF-scholarly_paper}
    {Scholarly Paper only supports LNCS as document class.}{}\stop%
}
\end{ltx}›

  We encourage this clear and machine-checkable enforcement of restrictions while, at the same
  time, we also encourage to provide a package option to overwrite them. The latter allows 
  inherited ontologies to overwrite these restrictions and, therefore, to provide also support
  for additional document templates. For example, the ontology boxed_theory_text‹technical_report›
  extends the boxed_theory_text‹scholarly_paper› ontology and its LaTeX supports provides support
  for the boxed_latex‹scrrept›-class which is not supported by the LaTeX support for 
  boxed_theory_text‹scholarly_paper›.
›

(*<*)
end
(*>*)