From 229997d60ae34bb17570cbc97b80eed97ca69126 Mon Sep 17 00:00:00 2001
From: bu <wolff@lri.fr>
Date: Wed, 4 Apr 2018 16:25:33 +0200
Subject: [PATCH] Added open/close monitor syntax.

---
 Isa_DOF.thy                 | 12 +++++++++++-
 examples/simple/Article.thy | 27 ++++++++-------------------
 2 files changed, 19 insertions(+), 20 deletions(-)

diff --git a/Isa_DOF.thy b/Isa_DOF.thy
index b0a13f0..b73493b 100644
--- a/Isa_DOF.thy
+++ b/Isa_DOF.thy
@@ -11,7 +11,8 @@ 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*" "declare_reference"::thy_decl
+           "paragraph*"  "subparagraph*" "text*" 
+           "open_monitor" "close_monitor" "declare_reference"::thy_decl
            and
            "doc_class" :: thy_decl 
   
@@ -387,6 +388,15 @@ val _ =
     (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"
+    (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"
+    (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 f8e6f68..e81fd88 100644
--- a/examples/simple/Article.thy
+++ b/examples/simple/Article.thy
@@ -1,6 +1,8 @@
 theory Article 
   imports "../../ontologies/LNCS_onto"
 begin
+
+open_monitor[onto::article]  
   
 text*[tit::title]{* Using The Isabelle Ontology Framework*} 
   
@@ -36,28 +38,12 @@ subsection*[scholar_onto::example]{* A Scholar Paper: Eating one's own dogfood.
   
 subsection*[mathex_onto::example]{* Math-Exercise *}  
   
-subsection*[cenelec_onto::example]{* CENELEC  *}  
-
 section*[con::conclusion]{* Future Work: Monitoring Classes *}    
-text{* Lorem ipsum dolor sit amet, suspendisse non arcu malesuada mollis, nibh morbi, ...
-
-The control of monitors is done by the commands:
-\<bullet> open_monitor  <doc-class>
-\<bullet> close_monitor <doc-class> 
-where the automaton of the monitor class is expected
-to be in a final state.
-
-Monitors can be nested, so it is possible to "overlay" one or more monitoring 
-classes and imposing different sets of structural constraints in a 
-
-Classes neither directly or via inheritance indirectly
-mentioned in the monitor are @{bold \<open>nested\<close>}
-from a monitor and may occur freely. 
-*}
+text{* Lorem ipsum dolor sit amet, suspendisse non arcu malesuada mollis, nibh morbi, ... *}
 
 subsection*[related::related_work]{* Related Work *}
 text{* 
-\<bullet> XML and dtd's, 
+\<bullet> @{bold  \<open>XML\<close>} and dtd's, 
 \<bullet> OWL and Protege, 
 \<bullet> LaTeX setups such as ... 
   @{url "https://pdi.fbk.eu/technologies/tex-owl-latex-style-syntax-authoring-owl-2-ontologies"} 
@@ -66,8 +52,11 @@ text{*
 \<bullet> AADL Alisa, 
 \<bullet> RATP Ovado
 *}  
+  
 subsection{* Discussion *}  
- 
+text{* Lorem ipsum dolor sit amet, suspendisse non arcu malesuada mollis, nibh morbi, ... *}
+
+close_monitor[onto]  
   
 end