From b220233373387128b37c3e094a05ea5029d167d7 Mon Sep 17 00:00:00 2001
From: bu <wolff@lri.fr>
Date: Tue, 9 Oct 2018 15:56:17 +0200
Subject: [PATCH] =?UTF-8?q?doc=5Fitem=20creation=20detects=20enabled=20mon?=
 =?UTF-8?q?itors=20=E2=80=A6?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Isa_DOF.thy                               | 22 +++++++++++++++++++---
 examples/scholarly/IsaDofApplications.thy |  8 +++++---
 2 files changed, 24 insertions(+), 6 deletions(-)

diff --git a/Isa_DOF.thy b/Isa_DOF.thy
index c1109226..cf01e657 100644
--- a/Isa_DOF.thy
+++ b/Isa_DOF.thy
@@ -90,8 +90,8 @@ struct
                        |  SOME ({inherits_from=SOME (_,s'), ...}) => 
                                   s' = t orelse father_is_sub s' 
         in s = t orelse 
-           (t = default_cid andalso Symtab.defined tab s ) orelse
-           father_is_sub s
+           (t = default_cid  andalso Symtab.defined tab s ) orelse
+           (s <> default_cid andalso father_is_sub s)
         end
 
    type docobj =    {pos      : Position.T, 
@@ -119,6 +119,7 @@ struct
 
    type open_monitor_info = {enabled_for_cid : string list,
                              regexp_stack    : term list list (* really ? *)}
+
    type monitor_tab = open_monitor_info Symtab.table
 
    val  initial_monitor_tab:monitor_tab = Symtab.empty
@@ -166,6 +167,9 @@ fun upd_monitor_tabs f {docobj_tab,docclass_tab,ISA_transformer_tab, monitor_tab
              ISA_transformer_tab = ISA_transformer_tab, monitor_tab = f monitor_tab};
 
 
+fun get_enabled_for_cid  ({enabled_for_cid, regexp_stack }:open_monitor_info) =  enabled_for_cid
+fun get_regexp_stack     ({enabled_for_cid, regexp_stack }:open_monitor_info) =  regexp_stack
+
 
 (* doc-class-name management: We still use the record-package for internally 
    representing doc-classes. The main motivation is that "links" to entities are
@@ -177,6 +181,7 @@ fun upd_monitor_tabs f {docobj_tab,docclass_tab,ISA_transformer_tab, monitor_tab
    handling the identification does that already. *)
  
 fun is_subclass (ctxt) s t = is_subclass0(#docclass_tab(get_data ctxt)) s t
+fun is_subclass_global thy s t = is_subclass0(#docclass_tab(get_data_global thy)) s t
 
 fun type_name2doc_class_name thy str =  (*  Long_Name.qualifier *) str
 
@@ -845,7 +850,17 @@ fun calc_update_term thy cid_long (S:(string * Position.T * string * term)list)
              end   
      in Sign.certify_term thy  (fold read_assn S term) end
 
-
+fun register_oid_cid_in_open_monitors oid cid_long thy = 
+      let val {monitor_tab,...} = DOF_core.get_data_global thy
+          fun is_enabled (n, info) = 
+                         if exists (DOF_core.is_subclass_global thy cid_long) 
+                                   (DOF_core.get_enabled_for_cid info) 
+                         then SOME n 
+                         else NONE
+          val enabled_monitors = List.mapPartial is_enabled (Symtab.dest monitor_tab)
+          val _ = writeln "registrating ..." 
+          val _ = app (fn n => writeln(oid^" => "^n)) enabled_monitors;
+      in  thy end
 
 fun create_and_check_docitem is_monitor oid pos cid_pos doc_attrs thy = 
       let val id = serial ();
@@ -866,6 +881,7 @@ fun create_and_check_docitem is_monitor oid pos cid_pos doc_attrs thy =
                                                       value    = value_term,
                                                       id       = id,   
                                                       cid      = cid_long})
+              |> register_oid_cid_in_open_monitors oid cid_long
       end
 
 
diff --git a/examples/scholarly/IsaDofApplications.thy b/examples/scholarly/IsaDofApplications.thy
index ce401812..c60ebaa0 100644
--- a/examples/scholarly/IsaDofApplications.thy
+++ b/examples/scholarly/IsaDofApplications.thy
@@ -58,7 +58,8 @@ the document discourse.
 
 Such ontologies can be used for the scientific discourse within scholarly
 articles, mathematical libraries, and in the engineering discourse  
-of standardized software certification documents~@{cite "boulanger:cenelec-50128:2015" and "cc:cc-part3:2006"}. 
+of standardized software certification 
+documents~@{cite "boulanger:cenelec-50128:2015" and "cc:cc-part3:2006"}. 
 Further applications are the domain-specific discourse in juridical texts or medical reports.  
 In general, an ontology is a formal explicit description of \<^emph>\<open>concepts\<close> 
 in a domain of discourse (called \<^emph>\<open>classes\<close>), properties of each concept 
@@ -101,8 +102,8 @@ scenarios from the point of view of the ontology modeling. In @{docitem_ref (unc
 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>  
 
-section*[bgrnd::text_section,main_author="Some(@{docitem ''adb''}::author)"]\<open>
- Background: The Isabelle System \<close>
+section*[bgrnd::text_section,main_author="Some(@{docitem ''adb''}::author)"]
+        \<open> Background: The Isabelle System \<close>
 text*[background::introduction]\<open>
 While Isabelle is widely perceived as an interactive theorem prover
 for HOL (Higher-order Logic)~@{cite "nipkow.ea:isabelle:2002"}, we
@@ -255,6 +256,7 @@ Isabelle users to Isabelle users only.
 Of course, such references can be added easily and represent a particular strength  
 of \isadof.
 
+
 \begin{figure}
 \begin{isar}
 doc_class title =