New Structure discussed with adb, different shot in intro, ref to SEFM paper, first railroad dgm

examples/technical_report/IsaDof_Manual/01_Introduction.thy

@@ -43,11 +43,20 @@ it is an \<^emph>\<open>environment to write structured text\<close> which \<^em
 Isabelle/HOL definitions and proofs like mathematical articles, tech-reports and
 scientific papers---as the present one, which is written in \isadof 
 itself. \isadof is a plugin into the Isabelle/Isar
-framework in the style of~@{cite "wenzel.ea:building:2007"}.
+framework in the style of~@{cite "wenzel.ea:building:2007"}.\<close>
+
+
+text\<open>This manual adresses at three different types of users:
+\<^enum> users that just want to edit a core document, be it for a paper or a technical report,
+  using a given ontology,
+\<^enum> users that want to develop ontologies and/or modify the generated PDF-presentations,
+\<^enum> users that want to add text-elements or new features to \isadof.
+
+This manual gives priority to the former two groups; users with an interest in \isadof implementation
+might find complementary information in  @{cite "brucker.wolff19:isadof-design-impl:2019"}.
+
 \<close>
 
-
-
 (* declaring the forward references used in the subsequent section *)  
 (*<*)
 declare_reference*[bgrnd::text_section]
@@ -57,14 +66,18 @@ declare_reference*[ontopide::text_section]
 declare_reference*[conclusion::text_section]
 (*>*)
 text*[plan::introduction]\<open> The plan of the paper is follows: we start by introducing  the underlying 
-Isabelle sytem (@{docitem_ref (unchecked) \<open>bgrnd\<close>}) followed by presenting the 
-essentials of  \isadof and its ontology language (@{docitem_ref (unchecked) \<open>isadof\<close>}). 
-It follows @{docitem_ref (unchecked) \<open>casestudies\<close>}, where we present three application 
+Isabelle system (@{docitem_ref (unchecked) \<open>bgrnd\<close>}) followed guided tour or tutorial
+adressing the needs of the first intended user group. 
+It follows the chapter @{docitem_ref (unchecked) \<open>isadof\<close>} for the second user group 
+with essentials of  \isadof and its ontology language (@{docitem_ref (unchecked) \<open>isadof\<close>}). 
+
+XXX
+
+It follows @{docitem_ref (unchecked) \<open>casestudies\<close>}, where we present three application
 scenarios from the point of view of the ontology modeling. In @{docitem_ref (unchecked) \<open>ontopide\<close>}
 we discuss the user-interaction generated from the ontological definitions.  Finally, we draw 
 conclusions  and discuss related work in @{docitem_ref (unchecked) \<open>conclusion\<close>}. \<close>  
 
-
 (*<*) 
 end
 (*>*) 

examples/technical_report/IsaDof_Manual/03_GuidedTour.thy

@@ -1,10 +1,10 @@
 (*<*)
-theory "04_IsaDofCaseStudies"
-  imports "03_IsaDof"
+theory "03_GuidedTour"
+  imports "02_Background"
 begin
 (*>*)
 
-chapter*[casestudies::example,main_author="Some(@{docitem ''adb''}::author)"]\<open> \isadof Case Studies \<close>
+chapter*[casestudies::example,main_author="Some(@{docitem ''adb''}::author)"]\<open> \isadof: A Guided Tour \<close>
    
 text\<open> In this section, we will use the \isadof document ontology language
 for three different application scenarios: for scholarly papers, for mathematical 
@@ -348,11 +348,11 @@ doc_class srac = ec  +
 \end{isar}
 \<close>
    
-chapter*[ontopide::technical]\<open> Ontology-based IDE support \<close>  
+section*[ontopide::technical]\<open> Ontology-based IDE support \<close>  
 text\<open> We present a selection of interaction scenarios  @{example \<open>scholar_onto\<close>}
 and @{example \<open>cenelec_onto\<close>} with Isabelle/PIDE instrumented by \isadof. \<close>
 
-section*[scholar_pide::example]\<open> A Scholarly Paper \<close>  
+subsection*[scholar_pide::example]\<open> A Scholarly Paper \<close>  
 text\<open> In \autoref{fig-Dogfood-II-bgnd1} and \autoref{fig-bgnd-text_section} we show how
 hovering over links permits to explore its meta-information. 
 Clicking on a document class identifier permits to hyperlink into the corresponding
@@ -391,7 +391,7 @@ non-compatible type, the text is not validated.  \<close>
 
 figure*[figDogfoodVIlinkappl::figure,relative_width="80",src="''figures/Dogfood-V-attribute''"]
        \<open> Exploring an attribute (hyperlinked to the class). \<close> 
-section*[cenelec_pide::example]\<open> CENELEC  \<close>
+subsection*[cenelec_pide::example]\<open> CENELEC  \<close>
 declare_reference*[figfig3::figure]  
 text\<open> The corresponding view in @{docitem_ref (unchecked) \<open>figfig3\<close>} shows core part of a document,  
 coherent to the @{example \<open>cenelec_onto\<close>}. The first sample shows standard Isabelle antiquotations 

examples/technical_report/IsaDof_Manual/04_RefMan.thy

@@ -1,11 +1,11 @@
 (*<*)
-theory "03_IsaDof"
-  imports "02_Background"
+theory "04_RefMan"
+  imports "03_GuidedTour"
 begin
 (*>*)
 
-chapter*[isadof::technical,main_author="Some(@{docitem ''adb''}::author)"]
-\<open> \isadof : Design and Use of its Commands\<close>
+chapter*[isadof::technical,main_author="Some(@{docitem ''bu''}::author)"]
+\<open> \isadof : Syntax and Semantics of Commands\<close>
    
 text\<open> An \isadof document consists of three components: 
 \<^item> the \<^emph>\<open>ontology definition\<close> which is an Isabelle theory file with definitions
@@ -61,9 +61,19 @@ While document classes and their inheritance relation structure meta-data of tex
 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 that must belong to the corresponding classes. 
-
 \<close>
 
+text\<open>
+\<^rail>\<open>
+    (@@{command "chapter*"} | @@{command "section*"} | @@{command "subsection*"} |
+      @@{command "subsubsection*"} | @@{command "paragraph*"} | @@{command "subparagraph*"})
+    (@@{command "text*"} | @@{command "figure*"} | @@{command "side_by_side_figure*"} | 
+      @@{command "open_monitor*"} | @@{command "close_monitor*"} | 
+      @@{command "update_instance*"} | @@{command "declare_reference*"})
+  \<close>              
+\<close>
+
+
 section*[install::technical]\<open>Installation\<close>
 text\<open>
 To start using \isadof, one creates an Isabelle project (with the name 
@@ -83,7 +93,6 @@ article in PDF using the  following command:
 
 section*["odl-design"::technical]\<open>The Design of ODL\<close>
 
-declare_reference*[scholar_onto::example]
 subsection*[onto_future::technical]\<open> Monitor Classes \<close>  
 (*
 text\<open> Besides sub-typing, there is another relation between

examples/technical_report/IsaDof_Manual/05_IsaDofLaTeX.thy

@@ -1,6 +1,6 @@
 (*<*)
 theory "05_IsaDofLaTeX"
-  imports "04_IsaDofCaseStudies"
+  imports "04_RefMan"
 begin
 (*>*)
 

examples/technical_report/IsaDof_Manual/IsaDofManual.thy

@@ -4,6 +4,9 @@ theory IsaDofManual
 begin
 (*<*) 
 
+
+
+
 text*[bib::bibliography]\<open>References\<close>
 
 (*<*)

examples/technical_report/IsaDof_Manual/document/preamble.tex

@@ -51,6 +51,7 @@
 
 \usepackage[caption]{subfig}
 \usepackage[size=footnotesize]{caption}
+\usepackage{railsetup}
 
 \newcommand{\ie}{i.e.}
 \newcommand{\eg}{e.g.}

examples/technical_report/IsaDof_Manual/document/root.bib

@@ -351,4 +351,44 @@
  acmid = {3204223},
  publisher = {Springer-Verlag},
  address = {Berlin, Heidelberg},
-} 
+} 
+
+@incollection{brucker.wolff19:isadof-design-impl:2019,
+  abstract = {DOF is a novel framework for \emph{defining} ontologies and
+  \emph{enforcing} them during document development and document
+  evolution. A major goal of DOF is the integrated development of
+  formal certification documents (\eg, for Common Criteria or CENELEC
+  50128) that require consistency across both formal and informal
+  arguments.
+
+  To support a consistent development of formal and informal parts of
+  a document, we provide Isabelle/DOF, an implementation of DOF on top of
+  Isabelle/HOL.  \isadof is integrated into Isabelle's IDE, which
+  allows for smooth ontology development as well as immediate
+  ontological feedback during the editing of a document.
+
+  In this paper, we give an in-depth presentation of the design
+  concepts of DOF's Ontology Definition Language (ODL) and key
+  aspects of the technology of its implementation.  \isadof is the
+  first ontology language supporting machine-checked
+  links between the formal and informal parts in an LCF-style
+  interactive theorem proving environment.
+
+  Sufficiently annotated, large documents can easily be developed
+  collaboratively, while \emph{ensuring their consistency}, and the
+  impact of changes (in the formal and the semi-formal content) is
+  tracked automatically.},
+  address = {Heidelberg},
+  author = {Achim D. Brucker and Burkhart Wolff},
+  booktitle = {International Conference on Software Engineering and Formal Methods (SEFM)},
+  doi = {10.1007/978-3-319-96812-4_3},
+  keywords = {Isabelle, HOL, Ontologies, Certification},
+  language = {USenglish},
+  location = {Oslo, Norway},
+  number = {TO APPEAR},
+  pdf = {https://www.lri.fr/~wolff/papers/conf/2019-sefm-isa_dof-framework.pdf},
+  publisher = {Springer-Verlag},
+  series = {Lecture Notes in Computer Science},
+  title = {{I}sabelle/{DOF}: {D}esign and {I}mplementation},
+  year = {2019}
+}