From 99bdf17712f28788a7d40de60e25fd7173d54b51 Mon Sep 17 00:00:00 2001
From: bu <wolff@lri.fr>
Date: Wed, 18 Apr 2018 14:46:28 +0200
Subject: [PATCH] parsing and internal type-checking works. No integral type
 checking yet, and no execution.

---
 Isa_DOF.thy                 | 25 +++++++++++++------------
 examples/simple/Article.thy |  4 ++--
 2 files changed, 15 insertions(+), 14 deletions(-)

diff --git a/Isa_DOF.thy b/Isa_DOF.thy
index 0addd7b..e856250 100644
--- a/Isa_DOF.thy
+++ b/Isa_DOF.thy
@@ -356,10 +356,8 @@ fun enriched_document_command markdown (((((oid,pos),cid_pos),doc_attrs),
     val _ = Position.report pos (docref_markup true oid id pos);
             (* creates a markup label for this position and reports it to the PIDE framework;
                this label is used as jump-target for point-and-click feature. *)
-
-    fun enrich_trans  (SOME(cid,pos')) thy = 
-                           let val name = Context.theory_name thy 
-                               val _ = if not (DOF_core.is_defined_cid_global cid thy) 
+    fun handle_classref name (SOME(cid,pos')) thy = 
+                           let val _ = if not (DOF_core.is_defined_cid_global cid thy) 
                                        then error("document class undefined")
                                        else ()
                                val cid_long =  DOF_core.name2doc_class_name thy cid 
@@ -374,13 +372,20 @@ fun enriched_document_command markdown (((((oid,pos),cid_pos),doc_attrs),
                                                                    id=id,   cid=cid_long})
                                                              (thy)
                            end
-       | enrich_trans  NONE thy = 
-                           let val name = Context.theory_name thy 
-                           in  DOF_core.define_object_global 
+       | handle_classref name NONE thy = 
+                           DOF_core.define_object_global 
                                   (oid, {pos=pos, thy_name=name,
                                          id=id,   cid=DOF_core.default_cid}) 
                                (thy)
-                           end
+                          
+    fun enrich_trans class_ref thy = 
+          let val name = Context.theory_name thy 
+              fun read_assn  ((lhs, pos), rhs) = (Syntax.read_term_global thy lhs,
+                                                  Syntax.read_term_global thy rhs)
+              val assns = map (read_assn ) doc_attrs
+          in  thy |> handle_classref name class_ref
+          end
+    
     fun MMM(SOME(s,p)) = SOME(s^"XXX",p)
        |MMM(NONE)      = SOME("XXX",Position.id "")
   in     
@@ -527,10 +532,6 @@ ML{*
  val y = Type_Infer_Context.infer_types @{context} [(Syntax.parse_term @{context} "None")]
          handle   TYPE _ => error"bla"; 
 *)
-*} 
-ML{* type_of t'
-
-
 *}  
   
 ML{* 
diff --git a/examples/simple/Article.thy b/examples/simple/Article.thy
index 51aec7c..007054c 100644
--- a/examples/simple/Article.thy
+++ b/examples/simple/Article.thy
@@ -10,7 +10,7 @@ text*[tit::title]{* Using The Isabelle Ontology Framework*}
   
 text*[stit::subtitle] \<open>Linking the Formal with the Informal\<close>
   
-text*[auth1::author, affiliation="Université Paris-Sud"]\<open>Burkhart Wolff\<close>
+text*[auth1::author, affiliation="''Universit\\'e Paris-Sud''"]\<open>Burkhart Wolff\<close>
     
 text*[abs::abstract, keyword_list="[]"] {* Isabelle/Isar is a system 
 framework with many similarities to Eclipse; it is mostly known as part of 
@@ -31,7 +31,7 @@ sed nibh ut lorem integer, maecenas sed mi purus non nunc, morbi pretium tortor.
 section*[bgrnd::text_section]{* Background: Isabelle and Isabelle_DOF *}  
 text{* As mentioned in @{introduction \<open>intro\<close>} ... *} 
 
-  term "a + b = b + a"
+term "a + b = b + a"
 
 (*
 @{term ''a + b = b + a''}