diff --git a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy index c5e90eae..e33072ce 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy @@ -13,7 +13,7 @@ (*<*) theory - "03_GuidedTour" + "03_GuidedTour" imports "02_Background" "Isabelle_DOF.CENELEC_50128" @@ -383,24 +383,26 @@ doc_class text_section = text_element + The \level\-attibute \<^index>\level\ enables doc-notation support for headers, chapters, sections, and subsections; we follow here the \<^LaTeX> terminology on levels to which \<^isadof> is currently targeting at. -The values are interpreted accordingly to the \<^LaTeX> standard. +The values are interpreted accordingly to the \<^LaTeX> standard. The correspondance between the levels +and the structural entities is summarized as follows: -\<^enum> part \<^index>\part\ \<^bigskip>\<^bigskip> \Some -1\ -\<^enum> chapter \<^index>\chapter\ \<^bigskip>\<^bigskip> \Some 0\ -\<^enum> section \<^index>\section\ \<^bigskip>\<^bigskip> \Some 1\ -\<^enum> subsection \<^index>\subsection\ \<^bigskip>\<^bigskip> \Some 2\ -\<^enum> subsubsection \<^index>\subsubsection\ \<^bigskip>\<^bigskip> \Some 3\ + \<^item> part \<^index>\part\ \<^bigskip>\<^bigskip> \Some -1\ \vspace{-1cm} + \<^item> chapter \<^index>\chapter\ \<^bigskip>\<^bigskip> \Some 0\ \vspace{-1cm} + \<^item> section \<^index>\section\ \<^bigskip>\<^bigskip> \Some 1\ \vspace{-1cm} + \<^item> subsection \<^index>\subsection\ \<^bigskip>\<^bigskip> \Some 2\ \vspace{-1cm} + \<^item> subsubsection \<^index>\subsubsection\ \<^bigskip>\<^bigskip> \Some 3\ \vspace{-0.1cm} Additional means assure that the following invariant is maintained in a document -conforming to @{theory \Isabelle_DOF.scholarly_paper\}: +conforming to \<^verbatim>\scholarly_paper\: \center {\level > 0\} \ text\ The rest of the ontology introduces concepts for \introductions\, \conclusion\, \related_work\, -\bibliography\ etc. More details can be found in \ +\bibliography\ etc. More details can be found in \<^verbatim>\scholarly_paper\ contained ion the +theory @{theory \Isabelle_DOF.scholarly_paper\}. \ -subsection\Writing Academic Publications `I : A Freeform Mathematics Text \ +subsection\Writing Academic Publications I : A Freeform Mathematics Text \ text*[csp_paper_synthesis::technical, main_author = "Some bu"]\We present a typical mathematical paper focussing on its form, not refering in any sense to its content which is out of scope here. As mentioned before, we chose the paper~@{cite "taha.ea:philosophers:2020"} for this purpose, @@ -408,8 +410,8 @@ which is written in the so-called free-form style: Formulas are superficially pa type-setted, but no deeper type-checking and checking with the underlying logical context is undertaken. -The corpus of the beginning looks like this (the setup seaquence is described later):\ -(* . Focus: Mathematical content. Definition, theorem, and citations... *) +The corpus of the paper beginning looks like this (the setup sequence is described later). \ + figure*[fig0::figure,spawn_columns=False,relative_width="95",src="''figures/header_CSP_source.png''"] \ A mathematics paper as a document source ... \ text\The document build process converts this to the following \<^pdf>-output:\ @@ -428,23 +430,19 @@ text\The paper proceeds by providing instances for introduction, technical We would like to concentrate on one --- mathematical paper oriented --- detail in the ontology \<^verbatim>\scholarly_paper\: @{theory_text [display] -\doc_class technical = text_section + - . . . +\doc_class technical = text_section + . . . type_synonym tc = technical (* technical content *) datatype math_content_class = "defn" | "axm" | "thm" | "lem" | "cor" | "prop" | ... -doc_class math_content = tc + - ... +doc_class math_content = tc + ... doc_class "definition" = math_content + - mcc :: "math_content_class" <= "defn" - ... + mcc :: "math_content_class" <= "defn" ... doc_class "theorem" = math_content + - mcc :: "math_content_class" <= "thm" - ... + mcc :: "math_content_class" <= "thm" ... \}\ text\The class \<^verbatim>\technical\ regroups a number of text-elements that contain typical @@ -473,28 +471,45 @@ accepts any offered event, wheras \CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P\< *) (* alternative *) -text\For example, this allows the following presentation in the integrated source:\ figure*[fig01::figure,spawn_columns=False,relative_width="95",src="''figures/definition-use-CSP.png''"] \ A screenshot of the integrated source with Definitions ...\ -text\which declares a \<^theory_text>\definition\ according to the \<^verbatim>\scholarly_paper\-ontology and uses it -subsequently. Note that the use in the ontology-generated antiquotation \<^theory_text>\@{definition X2}\ -is type-checked; referencing \<^verbatim>\X2\ as \<^theory_text>\theorem\ would be a type-error and be reported directly -by \<^isadof>. Note further, that if referenced correctly wrt. to the sub-typing hierarchy makes -\<^verbatim>\X2\ \<^emph>\navigable\ in Isabelle/jedit. +text\An example for a sequence of (Isabelle-formula-) texts, their ontological declarations as +\"definition"\s in terms of the \<^verbatim>\scholarly_paper\-ontology and their type-conform referencing +later is shown in \<^figure>\fig01\ in its presentation as the integrated source. -The correspondiong output looks as follows:\ +Note that the use in the ontology-generated antiquotation \<^theory_text>\@{definition X4}\ +is type-checked; referencing \<^verbatim>\X4\ as \<^theory_text>\theorem\ would be a type-error and be reported directly +by \<^isadof> in Isabelle/jEdit. Note further, that if referenced correctly wrt. to the sub-typing +hierarchy makes \<^verbatim>\X4\ \<^emph>\navigable\ in Isabelle/jedit; a click will cause the IDE to present the +defining occurrence of this text-element in the integrated source. + +Note, further, how \<^isadof>-commands like \<^theory_text>\text*\ interact with standard Isabelle document +antiquotations described in the Isabelle Isar Reference Manual in Chapter 4.2 in great detail. +We refrain ourselves here to briefly describe three freeform antiquotations used her in this text: + +\<^item> the freeform term antiquotation, also called \<^emph>\cartouche\, written by + \@{cartouche [style-parms] \. . .\\ or just by \\...\\ if the list of style parameters + is empty, +\<^item> the freeform antiquotation for theory fragments written \@{theory_text [style-parms] \...\\ + or just \<^verbatim>\\<^theory_text> \...\\ if the list of style parameters + is empty, +\<^item> the freeform antiquotations for verbatim, emphasized, bold, or footnote text elements. + +\<^isadof> text-elements such as \<^theory_text>\text*\ allow to have such standard term-antiquotations inside their +text, permitting to give the whole text entity a formal, referentiable status with typed meta- +information attached to it that may be used for presentation issues, search, or other technical +purposes. +\ figure*[fig02::figure,spawn_columns=False,relative_width="95",src="''figures/definition-use-CSP-pdf.png''"] \ ... and the corresponding pdf-oputput.\ -text\PROBLEM : SHOULD BE Definition 2 and NOT JUST A LINK ...\ + +text\The corresponding output of this snippet in the integrated source is shown in\<^figure>\fig02\. \ -subsection\Writing Academic Publications II (somewhat outdated)\ -text\ In our next example we concentrate on non-text-elements. Focus on Figures... - -\ - +subsection\More Freeform Publication Elements\ +(* figure*[fig1::figure,spawn_columns=False,relative_width="95",src="''figures/Dogfood-Intro''"] \ Ouroboros I: This paper from inside \ldots \ @@ -529,9 +544,9 @@ doc_class related_work = conclusion + main_author :: "author option" <= None \} - -Moreover, we model a document class for including figures (actually, this document class is already -defined in the core ontology of \<^isadof>): +*) +text\ In the following, we present some other text-elements provided by the Common Ontology Library +in @{theory "Isabelle_DOF.Isa_COL"}. it provides a document class for figures: @{boxed_theory_text [display]\ datatype placement = h | t | b | ht | hb @@ -546,24 +561,38 @@ figure*[fig_figures::figure,spawn_columns=False,relative_width="85",src="''figur \ Ouroboros II: figures \ldots \ text\ - The document class \<^boxed_theory_text>\figure\ (supported by the \<^isadof> command + The document class \<^boxed_theory_text>\figure\ (supported by the \<^isadof> command abbreviation \<^boxed_theory_text>\figure*\) makes it possible to express the pictures and diagrams - such as @{docitem \fig_figures\}. + as shown in \<^figure>\fig_figures\, which presents its own representation in the + integrated source as screenshot.\ - Finally, we define a monitor class definition that enforces a textual ordering +text\ + Finally, we define a \<^emph>\monitor class\ \<^index>\monitor class\ that enforces a textual ordering in the document core by a regular expression: -@{boxed_theory_text [display]\ -doc_class article = - style_id :: string <= "''LNCS''" - version :: "(int \ int \ int)" <= "(0,0,0)" - where "(title ~~ \subtitle\ ~~ \author\$^+$+ ~~ abstract ~~ - introduction ~~ \technical || example\$^+$ ~~ conclusion ~~ - bibliography)" -\} + @{boxed_theory_text [display]\ + doc_class article = + style_id :: string <= "''LNCS''" + version :: "(int \ int \ int)" <= "(0,0,0)" + where "(title ~~ \subtitle\ ~~ \author\$^+$+ ~~ abstract ~~ + introduction ~~ \technical || example\$^+$ ~~ conclusion ~~ + bibliography)" + \} + + In a integrated document source, the body of the content can be paranthesized into: + + @{boxed_theory_text [display]\ + open_monitor* [this::article] + ... + close_monitor*[this] + \} + + which signals to \<^isadof> begin and end of the part of the integrated document + in which the text-elements are expected to appear in a fixed ontological ordering. \ -subsection*[scholar_pide::example]\Editing Support for Academic Papers\ +subsection*[scholar_pide::example]\Navigation Support induced by an Ontology\ + side_by_side_figure*[exploring::side_by_side_figure,anchor="''fig-Dogfood-II-bgnd1''", caption="''Exploring a reference of a text-element.''",relative_width="48", src="''figures/Dogfood-II-bgnd1''",anchor2="''fig-bgnd-text_section''", @@ -585,7 +614,7 @@ text\ attribute-definition (which is qualified in order to disambiguate; \autoref{fig:Dogfood-V-attribute}). \ -(* Bu : This autoref stuff could be avoided if we would finally have monitors... *) +(* Bu : This autoref stuff could be avoided if we would finally have monitors over figures... *) figure*[figDogfoodVIlinkappl::figure,relative_width="80",src="''figures/Dogfood-V-attribute''"] \ Exploring an attribute (hyperlinked to the class). \