From 2e097e6b3c302d6b5944f355508f1cdb8a5bd331 Mon Sep 17 00:00:00 2001
From: bu <wolff@lri.fr>
Date: Tue, 11 Sep 2018 14:15:11 +0200
Subject: [PATCH] rough, non-functional implementation of ISA docitem

---
 Isa_DOF.thy                                       | 15 ++++++++++++---
 examples/conceptual/InnerSyntaxAntiquotations.thy |  4 +++-
 2 files changed, 15 insertions(+), 4 deletions(-)

diff --git a/Isa_DOF.thy b/Isa_DOF.thy
index c4f419c..cd49eb1 100644
--- a/Isa_DOF.thy
+++ b/Isa_DOF.thy
@@ -548,20 +548,28 @@ fun ML_isa_check_file thy (term, pos) =
   in  ML_isa_check_generic check thy (term, pos) end;
 
 
-
 fun ML_isa_id thy (term,pos) = SOME term
 
+
+fun ML_isa_check_docitem thy (term, pos) =
+  let fun check thy (name, _) = if DOF_core.is_declared_oid_global name thy then ()
+                                else err ("faulty reference to docitem: "^name) pos
+  in  ML_isa_check_generic check thy (term, pos) end 
+(* does not work - must transform type to get the term right. *)
+
+
 end; (* struct *)
                                                             
 \<close>
 
 
 subsection\<open> Isar - Setup\<close>
+
 setup\<open>DOF_core.update_isa_global("typ"    ,ISA_core.ML_isa_check_typ) \<close>     
 setup\<open>DOF_core.update_isa_global("term"   ,ISA_core.ML_isa_check_term) \<close>     
 setup\<open>DOF_core.update_isa_global("thm"    ,ISA_core.ML_isa_check_thm) \<close>     
 setup\<open>DOF_core.update_isa_global("file"   ,ISA_core.ML_isa_check_file) \<close>     
-setup\<open>DOF_core.update_isa_global("docitem",ISA_core.ML_isa_id)\<close>     
+setup\<open>DOF_core.update_isa_global("docitem",ISA_core.ML_isa_check_docitem)\<close>     
 
 
 section\<open> Syntax for Annotated Documentation Commands (the '' View'' Part I) \<close>
@@ -763,7 +771,8 @@ fun update_instance_command  (((oid:string,pos),cid_pos),
                          else error("incompatible classes:"^cid^":"^cid_long)
                  fun markup2string x = XML.content_of (YXML.parse_body x)
 
-                 fun conv_attrs (((lhs, pos), opn), rhs) = (markup2string lhs,pos,opn, Syntax.read_term_global thy rhs)
+                 fun conv_attrs (((lhs, pos), opn), rhs) = (markup2string lhs,pos,opn, 
+                                                            Syntax.read_term_global thy rhs)
                  val assns' = map conv_attrs doc_attrs
                  val def_trans = #1 o (calc_update_term thy cid_long assns')
           in     
diff --git a/examples/conceptual/InnerSyntaxAntiquotations.thy b/examples/conceptual/InnerSyntaxAntiquotations.thy
index bc2eb84..9d10e36 100644
--- a/examples/conceptual/InnerSyntaxAntiquotations.thy
+++ b/examples/conceptual/InnerSyntaxAntiquotations.thy
@@ -13,7 +13,9 @@ lemma murks : "T = {ert,dfg}" sorry
 
 text*[xcv::F, u="@{file ''./examples/conceptual/Attributes.thy''}"]\<open>Lorem ipsum ...\<close>
 
-text*[xcv1::F, r="[@{thm ''HOL.refl''}, @{thm ''InnerSyntaxAntiquotations.murks''}]", 
+text*[xcv1::F, r="[@{thm ''HOL.refl''}, 
+                   @{thm ''InnerSyntaxAntiquotations.murks''}]", 
+               b="{(@{docitem ''xcv''},@{docitem ''xcv''})}",   (* lamentable ! No typecheck.*)
                s="[@{typ ''int list''}]"]\<open>Lorem ipsum ...\<close>