Syntax for += works finally.

Examples here and there…

Isa_DOF.thy

@@ -9,12 +9,17 @@ text{* In this section, we develop on the basis of a management of references Is
 that provide direct support in the PIDE framework. *}  
   
 theory Isa_DOF   (* Isabelle Document Ontology Framework *)
-  imports  Main (* Isa_MOF *)
-  keywords "section*"    "subsection*"   "subsubsection*" 
-           "paragraph*"  "subparagraph*" "text*" 
-           "open_monitor*" "close_monitor*" "declare_reference*" 
+  imports  Main  (* Isa_MOF *)
+  keywords "+=" ":="
+
+  and      "section*"    "subsection*"   "subsubsection*" 
+           "paragraph*"  "subparagraph*" "text*"  ::thy_decl
+           
+  and      "open_monitor*" "close_monitor*" "declare_reference*" 
            "update_instance*" "doc_class" ::thy_decl
-          
+
+  and      "lemma*" ::thy_decl
+           
   
 begin
   
@@ -377,22 +382,10 @@ val attribute =
 
 val attribute_upd  : (((string * Position.T) * string) * string) parser =
     Parse.position Parse.const 
-    -- ( Parse.$$$ "+" ||  Parse.$$$ ":")  (* + still does not work ... Yuck ! ! !*)
-    --| Parse.$$$ "="  
-    (*
-    -- ( Parse.keyword_improper "+" ||  Parse.keyword_improper ":")  (* + still does not work ... *)
-    --| Parse.keyword_improper "="  
-     *)
-    (* -- ( Parse.keyword_with (fn x => "+=" = x) ||  Parse.keyword_with (fn x=> ":=" = x)) *) 
+    -- (@{keyword "+="} || @{keyword ":="})
     -- Parse.!!! Parse.term;
-(*
-Token.T list ->
-  (((string * Position.T) * string) * string) *
-  Token.T list*)
 
-(*
-Scan.optional (Args.parens (Args.$$$ defineN || Args.$$$ uncheckedN)
-*)
+(* Scan.optional (Args.parens (Args.$$$ defineN || Args.$$$ uncheckedN) *)
 val reference =
     Parse.position Parse.name 
     -- Scan.option (Parse.$$$ "::" |-- Parse.!!! (Parse.position Parse.name));
@@ -548,6 +541,13 @@ val _ =
                        "close a document reference monitor"
                        (attributes >> (fn (((oid,pos),cid),doc_attrs) => 
                                           (Toplevel.theory (I)))); (* dummy so far *)
+
+val _ =
+  Outer_Syntax.command @{command_keyword "lemma*"} 
+                       "close a document reference monitor"
+                       (attributes >> (fn (((oid,pos),cid),doc_attrs) => 
+                                          (Toplevel.theory (I)))); (* dummy/fake so far *)
+
 val _ =
   Outer_Syntax.command @{command_keyword "update_instance*"} 
                        "update meta-attributes of an instance of a document class"
@@ -556,6 +556,8 @@ val _ =
 end (* struct *)
 
 *}
+
+lemma murx : "XXX" sorry
   
 section{* Syntax for Ontological Antiquotations (the '' View'' Part II) *}
   
@@ -651,12 +653,6 @@ val _ = Theory.setup((docitem_ref_antiquotation @{binding docref} DOF_core.defau
 end (* struct *)
 *}
 
-ML{*
-      val count = Unsynchronized.ref (0 - 1);
-Unsynchronized.inc count;
-Unsynchronized.inc count
-
- *}
   
 section{* Syntax for Ontologies (the '' View'' Part III) *} 
 ML{* 

examples/simple/Article.thy

@@ -59,7 +59,7 @@ val a $ b $ c = @{term "X\<lparr>affiliation:='' ''\<rparr>"};
   
 term "scholarly_paper.author.affiliation_update"
 term "scholarly_paper.abstract.keywordlist_update"
-term "scholarly_paper.introduction.comment2_update"
+term "scholarly_paper.introduction.comment_update"
 ML{* val a $ b $ c = @{term "X\<lparr>affiliation:='' ''\<rparr>"}; fold;
 *}
 ML{* !AnnoTextelemParser.SPY;
@@ -68,15 +68,12 @@ fun convert((Const(s,_),_), t) X = Const(s^"_update", dummyT)
                                $ X
 val base = @{term "undefined"}
 val converts = fold convert (!AnnoTextelemParser.SPY) base
-ML{*   open Thm; varifyT_global ; 
-*}  
-  
+ 
 
 
 
   
 term "scholarly_paper.author.affiliation_update"
-term "scholarly_paper.abstract.keyword_list_update"
 term "scholarly_paper.introduction.comment_update"
   
 term "\<lparr>author.tag_attribute=undefined,email=''dfg'',orcid='''',affiliation=undefined\<rparr>"
@@ -91,7 +88,16 @@ val x = @{code "HORX"}
 
 section*[ontomod::technical]{* Modeling Ontologies in Isabelle_DOF *} 
 text{* Lorem ipsum dolor sit amet, suspendisse non arcu malesuada mollis, nibh morbi,*}
+
+lemma some_lemma : "P" sorry
   
+update_instance*[ontomod, formula := "[@{thm ''some_lemma''}]"] 
+
+lemma another_lemma : "Q" sorry
+  
+update_instance*[ontomod, formula += "[@{thm ''another_lemma''}]"] 
+
+    
 text*[x]{* @{technical \<open>ontomod\<close>} @{introduction \<open>bgrnd\<close>}*}
   
 subsection*[scholar_onto::example]{* A Scholar Paper: Eating one's own dogfood. @{technical \<open>ontomod\<close>} *}  

ontologies/CENELEC_50126.thy

@@ -10,14 +10,12 @@ Common Criteria identifies:
    order of category instances in the overall document as a regular language)
  *}  
 
+text_raw{*\snip{appendix.tex}{1}{1}{%*} 
+  
 theory CENELEC_50126
   imports "../Isa_DOF"
 begin
-  
-text_raw{*\snip{appendix.tex}{1}{1}{%*} 
-  
-text{* m importe quoi *}
-
+ 
 text_raw{*}%endsnip*}
 
 

ontologies/mathex_onto.thy

@@ -5,7 +5,7 @@ begin
 
 doc_class Author =
    affiliation :: "string"
-  email :: "string"
+   email :: "string"
 
 datatype Subject =
   algebra | geometry | statistical
@@ -13,6 +13,20 @@ datatype Subject =
 datatype Level =
   oneStar | twoStars | threeStars
 
+text{* In our scenario, content has three different types of addressees: 
+\<^item> the @{emph \<open>examiner\<close>}, i.e. the author of the exam, 
+\<^item> the @{emph \<open>student\<close>}, i.e. the addressee of the exam, 
+\<^item> the @{emph \<open>validator\<close>}, i.e. a person that checks the exam for
+  feasibility and non-ambiguity.
+
+Note that the latter quality assurance mechanism is used in many universities,
+where for organizational reasons the execution of an exam takes place in facilities
+where the author of the exam is not expected to be physically present.
+ *}  
+  
+datatype ContentClass =   
+  examiner | validator | student
+  
 datatype Grade =
   A1 | A2 | A3
 
@@ -23,12 +37,16 @@ doc_class Header =
 
 doc_class Question =
   level :: Level
-  mark :: integer
+  mark  :: integer
 
 doc_class Exercise= 
   content :: "(Question) list"
   mark :: integer
 
+doc_class Solution = 
+  content :: "(Question) list"
+  
+  
 doc_class MathExam=
   content :: "(Header + Author + Exercise) list"
   where "((Author)+  ~

ontologies/scholarly_paper.thy

@@ -34,7 +34,7 @@ doc_class introduction = text_section +
 
 doc_class technical = text_section +
    definition_list :: "string list" <=  "[]"
-   formula :: "term list"
+   formula :: "thm list"
    
 text{* A very rough formatting style could be modeled as follows:*}