diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy index 594858b..7d646f9 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy @@ -88,9 +88,9 @@ text\ are coupled with \<^emph>\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> stylefiles which were included during Isabelle's - document generation process. This one-to-many mapping implies a certain technical - organisation and some resulting restrictions described in @{technical (unchecked) \infrastructure\} - in more detail. + document generation process. This mapping is potentially a one-to-many mapping; + this implies a certain technical organisation and some resulting restrictions + described in @{technical (unchecked) \infrastructure\} in more detail. \ section\The Ontology Definition Language (ODL)\ @@ -203,7 +203,7 @@ text\ text\ Advanced ontologies can, \<^eg>, use recursive function definitions with pattern-matching~@{cite "kraus:defining:2020"}, extensible record - pecifications~@{cite "wenzel:isabelle-isar:2020"}, and abstract type declarations. + specifications~@{cite "wenzel:isabelle-isar:2020"}, and abstract type declarations. \ text\Note that \<^isadof> works internally with fully qualified names in order to avoid confusions @@ -330,22 +330,96 @@ is currently only available in the SML API's of the kernel. | @@{command "print_doc_items"} | @@{command "check_doc_global"}\ \<^item> \<^isadof> \macro_command\ : - \<^rail>\ @@{command "define_shortcut*"} name ('\' | '==') '\' string '\' + \<^rail>\ @@{command "define_shortcut*"} name ('\' | '==') '\' string '\' | @@{command "define_macro*"} name ('\' | '==') \ '\' string '\' '_' '\' string '\' \ \ +text\Recall that with the exception of \<^theory_text>\text* \ \, all \<^isadof> commands were mapped to visible +layout (such as \<^LaTeX>); these commands have to be wrapped into + \<^verbatim>\(*<*) ... (*>*)\ brackets if this is undesired. \ + subsection\Ontologic Text-Elements and their Management\ +text\ \<^theory_text>\text*[oid::cid, ...] \\\ \ text \ \\\ \ is the core-command of \<^isadof>: it permits to create + an object of meta-data belonging to the class \<^theory_text>\cid\. This is viewed as the \<^emph>\definition\ of +an instance of a document class. This instance object is attached to the text-element +and makes it thus "trackable" for \<^isadof>, \<^ie>, it can be referenced via the \<^theory_text>\oid\, its attributes +can be set by defaults in the class-definitions, or set at creation time, or modified at any +point after creation via \<^theory_text>\update_instance*[oid, ...]\. The \<^theory_text>\class_id\ is syntactically optional; +if ommitted, an object belongs to an anonymous superclass of all classes. +The \<^theory_text>\class_id\ is used to generate a \<^emph>\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 \<^theory_text>\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 \<^theory_text>\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 \<^theory_text>\cid\, there exists a text antiquotation of the form \<^theory_text>\ @{cid \oid\} \. +The precise presentation is decided in the \<^emph>\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 \<^theory_text>\ @{cid (unchecked) \oid\} \. + +% there should also exist a *term* antiquotation ... +\ + +(*<*) +declare_reference*["sec:advanced"::technical] +(*>*) subsection\Status and Query Commands\ +text\\<^isadof> provides a number of inspection commands. +\<^item> \<^theory_text>\print_doc_classes\ allows to view the status of the internal + class-table resulting from ODL definitions, +\<^item> \<^ML>\DOF_core.print_doc_class_tree\ allows for presenting (fragments) of + class-inheritance trees (currently only available at ML level), +\<^item> \<^theory_text>\print_doc_items\ allows to view the status of the internal + object-table of text-elements that were tracked, and +\<^item> \<^theory_text>\check_doc_global\ checks if all declared object references have been + defined, and all monitors are in a final state and final invariant checks + on all objects are satisfied (cf. @{technical (unchecked) \sec:advanced\}) +\ subsection\Macros\ +text\There is a mechanism to define document-local short-cuts and macros which +were PIDE-supported but lead to an expansion in the integrated source; this feature +can be used to define +\<^item> \<^theory_text>\shortcuts\, \<^ie>, short names that were expanded to, for example, + \<^LaTeX>-code, +\<^item> \<^theory_text>\macro\'s (= parameterized short-cuts), which allow for + passing an argument to the expansion mechanism. +\ +text\Note that 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\ +\<^item> 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{}\ + \} +\<^item> non-checking macro: + @{theory_text [display] \ + define_macro* index \ \\index{\ _ \}\ + \} +\<^item> 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 + of the input syntax. +\ section\The Standard Ontology Libraries\ text\ We will describe the backbone of the Standard Library with the already mentioned hierarchy \<^verbatim>\COL\ (the common ontology library), \<^verbatim>\scholarly_paper\ (for MINT-oriented scientific papers), - \<^verbatim>\technical_report\ (for MINT-oriented technical reports), \<^verbatim>\technical_report\ (for MINT-oriented technical reports), and the example for a domain-specific ontology \<^verbatim>\CENELEC_50128\.\ @@ -509,7 +583,7 @@ doc_class "thms" = subsection\The Ontology \<^theory>\Isabelle_DOF.technical_report\\ -subsection\An Exampe for a Domain-Specific Ontology: \<^theory>\Isabelle_DOF.CENELEC_50128\\ +subsection\A Domain-Specific Ontology: \<^theory>\Isabelle_DOF.CENELEC_50128\\ subsubsection\Example: Text Elemens with Levels\ text\