From 027361fb03c2384f17bde2682cb39d8192b92e18 Mon Sep 17 00:00:00 2001
From: bu <wolff@lri.fr>
Date: Wed, 4 Apr 2018 17:04:19 +0200
Subject: [PATCH] unified syntax: renamed declare_reference open_monitor
 close_monitor into declare_reference* open_monitor* close_monitor* in order
 to simplify the task for Achim.

---
 Isa_DOF.thy                  |  8 ++++----
 examples/simple/Article.thy  | 24 +++++++++++++-----------
 ontologies/CENELEC_50126.thy |  2 +-
 3 files changed, 18 insertions(+), 16 deletions(-)

diff --git a/Isa_DOF.thy b/Isa_DOF.thy
index b73493b..8c859c2 100644
--- a/Isa_DOF.thy
+++ b/Isa_DOF.thy
@@ -12,7 +12,7 @@ theory Isa_DOF   (* Isabelle Document Ontology Framework *)
   imports  Main (* Isa_MOF *)
   keywords "section*"    "subsection*"   "subsubsection*" 
            "paragraph*"  "subparagraph*" "text*" 
-           "open_monitor" "close_monitor" "declare_reference"::thy_decl
+           "open_monitor*" "close_monitor*" "declare_reference*"::thy_decl
            and
            "doc_class" :: thy_decl 
   
@@ -384,17 +384,17 @@ val _ =
       >> enriched_document_command {markdown = false});
 
 val _ =
-  Outer_Syntax.command @{command_keyword "declare_reference"} "declare document reference"
+  Outer_Syntax.command @{command_keyword "declare_reference*"} "declare document reference"
     (attributes >> (fn (((oid,pos),cid),doc_attrs) =>  
                                   (Toplevel.theory (DOF_core.declare_object_global oid))));
 
 val _ =
-  Outer_Syntax.command @{command_keyword "open_monitor"} "open a document reference monitor"
+  Outer_Syntax.command @{command_keyword "open_monitor*"} "open a document reference monitor"
     (attributes >> (fn (((oid,pos),cid),doc_attrs) =>  
                                   (Toplevel.theory (DOF_core.declare_object_global oid))));
 
 val _ =
-  Outer_Syntax.command @{command_keyword "close_monitor"} "close a document reference monitor"
+  Outer_Syntax.command @{command_keyword "close_monitor*"} "close a document reference monitor"
     (attributes >> (fn (((oid,pos),cid),doc_attrs) => (Toplevel.theory (I)))); (* dummy so far *)
 
 end (* struct *)
diff --git a/examples/simple/Article.thy b/examples/simple/Article.thy
index e81fd88..fa6feff 100644
--- a/examples/simple/Article.thy
+++ b/examples/simple/Article.thy
@@ -1,9 +1,11 @@
+(* << *)  
 theory Article 
   imports "../../ontologies/LNCS_onto"
 begin
-
-open_monitor[onto::article]  
+(* >> *) 
   
+open_monitor*[onto::article]  
+
 text*[tit::title]{* Using The Isabelle Ontology Framework*} 
   
 text*[stit::subtitle] \<open>Linking the Formal with the Informal\<close>
@@ -12,14 +14,12 @@ text*[auth1::author, affiliation="Université Paris-Sud"]\<open>Burkhart Wolff\<
     
 text*[abs::abstract, keyword_list="[]"] {* Isabelle/Isar is a system 
 framework with many similarities to Eclipse; it is mostly known as part of 
-Isabelle/HOL, an interactive theorem proving and code generation
-environment. Recently, an Document Ontology Framework has been
-developed as a plugin in Isabelle/Isar, allowing to do both 
-conventional typesetting \emph{as well} as formal development.
-A particular asset is the possibility to control the links 
+Isabelle/HOL, an interactive theorem proving and code generation environment. 
+Recently, an Document Ontology Framework has been developed as a plugin in 
+Isabelle/Isar, allowing to do both conventional typesetting \emph{as well} 
+as formal development. A particular asset is the possibility to control the links 
 between the formal and informal aspects of a document
-via (a novel use of) Isabelle's antiquotation mechanism.
- *}
+via (a novel use of) Isabelle's antiquotation mechanism. *}
   
 section*[intro::introduction, comment="''This is a comment''"]{* Introduction *} 
 text{* Lorem ipsum dolor sit amet, suspendisse non arcu malesuada mollis, nibh morbi, 
@@ -56,7 +56,9 @@ text{*
 subsection{* Discussion *}  
 text{* Lorem ipsum dolor sit amet, suspendisse non arcu malesuada mollis, nibh morbi, ... *}
 
-close_monitor[onto]  
-  
+close_monitor*[onto]  
+
+(* << *)    
 end
+(* >> *)    
   
diff --git a/ontologies/CENELEC_50126.thy b/ontologies/CENELEC_50126.thy
index a2a770b..62ea09a 100644
--- a/ontologies/CENELEC_50126.thy
+++ b/ontologies/CENELEC_50126.thy
@@ -9,7 +9,7 @@ Common Criteria identifies:
   (for the moment: defined by regular expressions describing the
    order of category instances in the overall document as a regular language)
  *}  
-  
+
 theory CENELEC_50126
   imports "../Isa_DOF"
 begin