From 3b21df199bd605be4580ea65ffd2a2f1af9091e9 Mon Sep 17 00:00:00 2001
From: Burkhart Wolff <wolff@lri.fr>
Date: Wed, 21 Apr 2021 20:24:06 +0200
Subject: [PATCH] addded docitem ML antiquotation. (Kleine Fingeruebung).

---
 src/DOF/Isa_DOF.thy                      | 20 +++++++++++++++++---
 src/ontologies/Conceptual/Conceptual.thy |  3 ++-
 src/tests/TermAntiquotations.thy         |  4 +++-
 3 files changed, 22 insertions(+), 5 deletions(-)

diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy
index 6188ba5..7932c64 100755
--- a/src/DOF/Isa_DOF.thy
+++ b/src/DOF/Isa_DOF.thy
@@ -1647,8 +1647,8 @@ fun compute_trace_ML ctxt oid pos pos' =
         fun conv (Const(@{const_name "Pair"},_) $ Const(s,_) $ S) = (s, HOLogic.dest_string S)
     in  map conv (HOLogic.dest_list term) end
 
-val parse_oid = Scan.lift(Parse.position Args.name) 
-val parse_cid = Scan.lift(Parse.position Args.name) 
+val parse_oid  = Scan.lift(Parse.position Args.name) 
+val parse_cid  = Scan.lift(Parse.position Args.name) 
 val parse_oid' = Term_Style.parse -- parse_oid
 val parse_cid' = Term_Style.parse -- parse_cid
 
@@ -1664,6 +1664,18 @@ val parse_attribute_access' = Term_Style.parse -- parse_attribute_access
 fun attr_2_ML ctxt ((attr:string,pos),(oid:string,pos')) = (ML_Syntax.atomic o ML_Syntax.print_term) 
                                                            (compute_attr_access ctxt attr oid pos pos') 
 
+
+val TERM_STORE = let val dummy_term = Bound 0
+                 in  Unsynchronized.ref (dummy_term) end
+
+fun get_instance_value_2_ML ctxt (oid:string,pos) =
+    let val term = case DOF_core.get_value_global oid (Context.theory_of ctxt) of
+                    SOME(t) => t
+                  | NONE    => error "not an object id"
+        val _ = (TERM_STORE := term)  (* export to the ML Context *)
+    in  "! AttributeAccess.TERM_STORE" end
+
+
 fun trace_attr_2_ML ctxt (oid:string,pos) =
     let val print_string_pair = ML_Syntax.print_pair  ML_Syntax.print_string ML_Syntax.print_string
         val toML = (ML_Syntax.atomic o (ML_Syntax.print_list print_string_pair))
@@ -1686,7 +1698,9 @@ fun pretty_cid_style ctxt (style, (cid,pos)) =
 
 in
 val _ = Theory.setup 
-           (ML_Antiquotation.inline  \<^binding>\<open>docitem_attribute\<close> 
+           (ML_Antiquotation.inline  \<^binding>\<open>docitem\<close> 
+               (fn (ctxt,toks) => (parse_oid >> get_instance_value_2_ML ctxt) (ctxt, toks))  #>
+            ML_Antiquotation.inline  \<^binding>\<open>docitem_attribute\<close> 
                (fn (ctxt,toks) => (parse_attribute_access >>  attr_2_ML ctxt) (ctxt, toks))  #>
             ML_Antiquotation.inline  \<^binding>\<open>trace_attribute\<close>  
                (fn (ctxt,toks) => (parse_oid >> trace_attr_2_ML ctxt) (ctxt, toks)) #>
diff --git a/src/ontologies/Conceptual/Conceptual.thy b/src/ontologies/Conceptual/Conceptual.thy
index 135a891..556400e 100755
--- a/src/ontologies/Conceptual/Conceptual.thy
+++ b/src/ontologies/Conceptual/Conceptual.thy
@@ -76,11 +76,12 @@ ML\<open> Session.get_keywords(); (* this looks to be really session global. *)
 ML\<open> Thy_Header.get_keywords @{theory};(* this looks to be really theory global. *) \<close>
 *)
 
+open_monitor*[aaa::M]
 section*[test::A]\<open>Test and Validation\<close>
 text\<open>Defining some document elements to be referenced in later on in another theory: \<close>
 text*[sdf]\<open> Lorem ipsum @{thm refl}\<close> 
 text*[ sdfg :: F] \<open> Lorem ipsum @{thm refl}\<close>  
 text*[ xxxy ] \<open> Lorem ipsum @{F \<open>sdfg\<close>} rate @{thm refl}\<close>  
-
+close_monitor*[aaa]
 
 end     
diff --git a/src/tests/TermAntiquotations.thy b/src/tests/TermAntiquotations.thy
index ee8a72f..29130f2 100755
--- a/src/tests/TermAntiquotations.thy
+++ b/src/tests/TermAntiquotations.thy
@@ -79,8 +79,10 @@ a @{typ "C"}-type is required, but a  @{typ "G"}-type is offered which is legal
 \verb+Isa_DOF+ because of the sub-class relation between those classes: \<close>
 update_instance*[xcv4::F, b+="{(@{docitem ''xcv3''},@{docitem ''xcv5''})}"]
 
-text\<open>And here is the result on term level:\<close>
+text\<open>And here is the results of some ML-term antiquotations:\<close>
 ML\<open> @{docitem_attribute b::xcv4} \<close>
+ML\<open> @{docitem xcv4}              \<close>
+ML\<open> @{trace_attribute aaa}       \<close>
 
 end