From 029ae709e6f850570c10cb09d1933f187e24157a Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sun, 7 Feb 2021 20:01:43 +0000 Subject: [PATCH] Migrated \inlineltx{}, except when argument contained { or }. --- .../Isabelle_DOF-Manual/04_RefMan.thy | 62 +++++++++---------- 1 file changed, 30 insertions(+), 32 deletions(-) diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy index 4f58859e..a14feb47 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy @@ -114,9 +114,9 @@ text\ \<^emph>\is-a\ relation between classes; \<^item> classes may refer to other classes via a regular expression in a \<^emph>\where\ clause; - % TODO: - % Update to the new implementation. - % where is deprecated and the new implementation uses accepts and rejects. +(* % TODO: + % Update to the new implementation. + % where is deprecated and the new implementation uses accepts and rejects. *) \<^item> attributes may have default values in order to facilitate notation. \ @@ -149,9 +149,9 @@ text\ 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. - % TODO: - % Update to the new implementation. - % where is deprecated and the new implementation uses accepts and rejects. + (* % TODO: + % Update to the new implementation. + % where is deprecated and the new implementation uses accepts and rejects. *) 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>, @@ -177,9 +177,9 @@ text\ 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 for Burkhart Wolff. - % This phrase should be reviewed to clarify identifiers. - % Peculiarly, "and identifiers in \<^boxed_theory_text>\ ... \". + (* % TODO + % This phrase should be reviewed to clarify identifiers. + % Peculiarly, "and identifiers in \<^boxed_theory_text>\ ... \". *) \<^item> \tyargs\:\<^index>\tyargs@\tyargs\\ \<^rail>\ typefree | ('(' (typefree * ',') ')')\ \typefree\ denotes fixed type variable(\'a\, \'b\, ...) (see~@{cite "wenzel:isabelle-isar:2020"}) @@ -260,7 +260,7 @@ A document class\<^bindex>\document class\ can be defined using the 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\ + \inlineltx|\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 @@ -278,20 +278,20 @@ text\ 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 + 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 \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. - % TODO: - % For the "(written in \<^boxed_theory_text>\\ ... \\" part, to give some examples should be clearer. - +(* % TODO: + % For the "(written in \<^boxed_theory_text>\\ ... \\" part, to give some examples should be clearer. +*) Moreover, \<^isadof> also provides the following two variants of \inlineltx|\newisadof{}[]{}|: - \<^item> \inlineltx|\renewisadof{}[]{}|\<^index>\renewisadof@\inlineltx{\renewisadof}\ for re-defining + \<^item> \inlineltx|\renewisadof{}[]{}|\<^index>\renewisadof@\<^boxed_latex>\\renewisadof\\ for re-defining (over-writing) an already defined command, and - \<^item> \inlineltx|\provideisadof{}[]{}|\<^index>\provideisadof@\inlineltx{\provideisadof}\ for providing + \<^item> \inlineltx|\provideisadof{}[]{}|\<^index>\provideisadof@\<^boxed_latex>\\provideisadof\\ for providing a definition if it is not yet defined. \ text\ @@ -372,7 +372,7 @@ The precise presentation is decided in the \<^emph>\layout definitions\-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 ... +(* % there should also exist a *term* antiquotation ... *) \ (*<*) @@ -475,9 +475,9 @@ doc_class text_element = As mentioned in @{technical \sss\} (without explaining the origin of \<^typ>\text_element\) , \<^boxed_theory_text>\level\ defines the section-level (\<^eg>, using a \<^LaTeX>-inspired hierarchy: -from \<^boxed_theory_text>\Some -1\ (corresponding to \inlineltx|\part|) to -\<^boxed_theory_text>\Some 0\ (corresponding to \inlineltx|\chapter|, respectively, \<^boxed_theory_text>\chapter*\) -to \<^boxed_theory_text>\Some 3\ (corresponding to \inlineltx|\subsubsection|, respectively, +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 would require that technical text section are introduce by a section element). @@ -566,9 +566,9 @@ It extends \<^verbatim>\COL\ by the following concepts: } \end{minipage} \end{center} - +(* TODO: There are some slight problems in the hierarchy ... - +*) \ text\A pivotal abstract class in the hierarchy is: @@ -801,7 +801,7 @@ doc_class EC = AC + We now define the document representations, in the file \<^file>\../../../src/ontologies/CENELEC_50128/DOF-CENELEC_50128.sty\. Let us assume that we want to -register the definition of EC's in a dedicated table of contents (\inlineltx{tos}) +register the definition of EC's in a dedicated table of contents (\<^boxed_latex>\tos\) and use an earlier defined environment \inlineltx|\begin{EC}...\end{EC}| for their graphical representation. Note that the \inlineltx|\newisadof{}[]{}|-command requires the full-qualified names, \<^eg>, \<^boxed_theory_text>\text.CENELEC_50128.EC\ for the document class and @@ -892,7 +892,7 @@ schemata: \end{ltx} After the definition of the dispatcher, one can, optionally, define a custom representation - using the \inlineltx|newisadof|-command, as introduced in the previous section: + using the \<^boxed_latex>\newisadof\-command, as introduced in the previous section: \begin{ltx} \newisadof{section}[label=,type=][1]{% @@ -1258,7 +1258,7 @@ text\ \<^file>\../../../src/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 \inlineltx|\author| and a \inlineltx|\institution| statement, each of + 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: @@ -1278,12 +1278,12 @@ text\ } \end{ltx} -The new command \inlineltx|\addauthor| and a similarly defined command \inlineltx|\addaffiliation| +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 begin of the document -(\<^ie>, when \<^LaTeX>'s \inlineltx|\maketitle| is invoked) while \<^isadof> allows to define authors at +(\<^ie>, when \<^LaTeX>'s \<^boxed_latex>\\maketitle\ is invoked) while \<^isadof> allows to define authors at any place within a document: \begin{ltx} @@ -1311,8 +1311,8 @@ any place within a document: } \end{ltx} -Finally, the collected information is used in the \inlineltx|\author| command using the -\inlineltx|AtBeginDocument|-hook: +Finally, the collected information is used in the \<^boxed_latex>\\author\ command using the +\<^boxed_latex>\AtBeginDocument\-hook: \begin{ltx} \newcommand{\DOFauthor}{\author{\dof@author}} @@ -1348,7 +1348,7 @@ text\ 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 \inlineltx|scrrept|-class which is not supported by the \<^LaTeX> support for + for the \<^boxed_latex>\scrrept\-class which is not supported by the \<^LaTeX> support for \<^boxed_theory_text>\scholarly_paper\. \ @@ -1360,8 +1360,6 @@ text\ \ - - (*<*) end (*>*)