revisions of scholarly paper and report ontologies

examples/technical_report/IsaDof_Manual/IsaDofManual.thy

@@ -3,7 +3,7 @@ theory IsaDofManual
   imports "../../../ontologies/technical_report"
 begin
 
-open_monitor*[this::article] 
+open_monitor*[this::report] 
 (*>*)
 
 title*[tit::title]\<open>The \isadof User and Implementation Manual\<close> 

ontologies/scholarly_paper.thy

@@ -25,17 +25,20 @@ doc_class abstract =
 doc_class text_section = 
    main_author :: "author option"  <=  None
    fixme_list  :: "string list"    <=  "[]" 
+   level       :: "int  option"    <=  "None"   
+                                  (* we follow LaTeX terminology on levels 
+                                               part          = Some -1
+                                               chapter       = Some 0
+                                               section       = Some 1
+                                               subsection    = Some 2
+                                               subsubsection = Some 3
+                                      ... *)
+   (* for scholarly paper: invariant level > 0 *)
 
 doc_class introduction = text_section +
    comment :: string
    claims  :: "thm list"
 
-doc_class introduction_title = introduction +
-   fixme_list  :: "string list"    <=  "[]" 
-
-doc_class introduction_elem = introduction +
-   fixme_list  :: "string list"    <=  "[]" 
-
 doc_class technical = text_section +
    definition_list :: "string list" <=  "[]"
    formal_results  :: "thm list"
@@ -84,16 +87,14 @@ text \<open>underlying idea: a monitor class automatically receives a
 doc_class article = 
    style_id :: string                <= "''LNCS''"
    version  :: "(int \<times> int \<times> int)"  <= "(0,0,0)"
-   accepts "(title       ~~ 
-           \<lbrakk>subtitle\<rbrakk>   ~~
-           \<lbrace>author\<rbrace>\<^sup>+   ~~ 
-           abstract     ~~
-           introduction_title ~~ 
-           \<lbrace>introduction_elem\<rbrace>\<^sup>+ ~~ 
-           \<lbrace>technical || example\<rbrace>\<^sup>+ ~~
-           \<lbrakk>introduction\<rbrakk>   ~~
-           conclusion   ~~  
-           bibliography)"
+   accepts "(title        ~~ 
+            \<lbrakk>subtitle\<rbrakk>    ~~
+            \<lbrace>author\<rbrace>\<^sup>+     ~~ 
+            abstract      ~~
+            introduction  ~~ 
+            \<lbrace>technical || example\<rbrace>\<^sup>+ ~~
+            conclusion   ~~  
+            bibliography)"
 
 gen_sty_template
 

ontologies/technical_report.thy

@@ -4,15 +4,19 @@ theory technical_report
    imports "scholarly_paper"
 begin
 
+(* for reports paper: invariant: level \<ge> -1 *)
+
 doc_class table_of_contents =
-   depth       :: int <= 3
+   bookmark_depth :: int <= 3
+   depth          :: int <= 3
 
 doc_class front_matter = 
-   style :: string 
+   front_matter_style :: string    (* TODO Achim :::: *)
+
+doc_class index =
+   kind  :: "doc_class" 
+   level :: "int option"
 
-doc_class "chapter" = text_section +
-   style :: string 
-  
 doc_class report = 
    style_id :: string                <= "''LNCS''"
    version  :: "(int \<times> int \<times> int)"  <= "(0,0,0)"
@@ -25,7 +29,7 @@ doc_class report =
            introduction ~~ 
            \<lbrace>technical || example\<rbrace>\<^sup>+ ~~ 
            conclusion   ~~  
-           \<lbrakk>table_of_contents\<rbrakk>  ~~
+           \<lbrace>index\<rbrace>\<^sup>+  ~~  
            bibliography)"
 
 end