From 5eebf2ef5b77adf5df4c33b4de338f7cabee8956 Mon Sep 17 00:00:00 2001
From: bu <wolff@lri.fr>
Date: Tue, 11 Sep 2018 12:08:25 +0200
Subject: [PATCH] =?UTF-8?q?some=20more=20isa=E2=80=99s?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Isa_DOF.thy                                   | 35 ++++++++++++++-----
 .../conceptual/InnerSyntaxAntiquotations.thy  |  2 ++
 ontologies/Conceptual.thy                     |  1 +
 3 files changed, 30 insertions(+), 8 deletions(-)

diff --git a/Isa_DOF.thy b/Isa_DOF.thy
index 9fbdbcf3..c4f7c4c7 100644
--- a/Isa_DOF.thy
+++ b/Isa_DOF.thy
@@ -519,13 +519,31 @@ fun ML_isa_antiq check_file thy (name, pos) =
   in "Path.explode " ^ ML_Syntax.print_string (Path.implode path) end;
 
 
-fun ML_isa_file_string thy (term, pos) =
+fun ML_isa_check_generic check thy (term, pos) =
   let val name = (HOLogic.dest_string term
                   handle TERM(_,[t]) => error ("wrong term format: must be string constant: " 
-                                               ^ Syntax.string_of_term_global @{theory} t ))
-      val check = (SOME File.check_file)
-      val _ = check_path check (Proof_Context.init_global thy) Path.current (name, pos);
-  in SOME term end;
+                                               ^ Syntax.string_of_term_global thy t ))
+      val _ = check thy (name,pos)
+  in  SOME term end;  
+
+
+fun ML_isa_check_typ thy (term, pos) =
+  let fun check thy (name, _) = Syntax.parse_typ (Proof_Context.init_global thy) name 
+  in  ML_isa_check_generic check thy (term, pos) end 
+
+
+fun ML_isa_check_term thy (term, pos) =
+  let fun check thy (name, _) = Syntax.parse_term (Proof_Context.init_global thy) name 
+  in  ML_isa_check_generic check thy (term, pos) end 
+
+
+fun ML_isa_check_file thy (term, pos) =
+  let fun check thy (name, pos) = check_path (SOME File.check_file) 
+                                             (Proof_Context.init_global thy) 
+                                             (Path.current) 
+                                             (name, pos);
+  in  ML_isa_check_generic check thy (term, pos) end;
+
 
 fun ML_isa_id thy (term,pos) = SOME term
 
@@ -538,13 +556,14 @@ end; (* struct *)
 \<close>
 
 ML\<open>Syntax.parse_typ\<close>
+
 subsection\<open> Isar - Setup\<close>
-
-setup\<open>DOF_core.update_isa_global("file",ISA_core.ML_isa_file_string) \<close>     
+setup\<open>DOF_core.update_isa_global("file"   ,ISA_core.ML_isa_check_file) \<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("docitem",ISA_core.ML_isa_id)\<close>     
 
 
-
 section\<open> Syntax for Annotated Documentation Commands (the '' View'' Part I) \<close>
 
 ML\<open>
diff --git a/examples/conceptual/InnerSyntaxAntiquotations.thy b/examples/conceptual/InnerSyntaxAntiquotations.thy
index 52cc57f7..5b927b5b 100644
--- a/examples/conceptual/InnerSyntaxAntiquotations.thy
+++ b/examples/conceptual/InnerSyntaxAntiquotations.thy
@@ -11,5 +11,7 @@ Symtab.dest z;
 
 text*[xcv::F, u="@{file ''./examples/conceptual/Attributes.thy''}"]\<open>Lorem ipsum ...\<close>
 
+text*[xcv1::F, s="[@{typ ''int list''}]"]\<open>Lorem ipsum ...\<close>
+
 
 end
diff --git a/ontologies/Conceptual.thy b/ontologies/Conceptual.thy
index 99a4e8aa..4e041486 100644
--- a/ontologies/Conceptual.thy
+++ b/ontologies/Conceptual.thy
@@ -31,6 +31,7 @@ doc_class E = D +
 doc_class F  = 
    r :: "thm list"
    u :: "file"
+   s :: "typ list"
    b :: "(A \<times> C) set"         <= "{}"
 
 doc_class M =