From f01b36997edaeb8386db5b7496f6913d87f09e52 Mon Sep 17 00:00:00 2001
From: bu <wolff@lri.fr>
Date: Fri, 27 Apr 2018 12:05:22 +0200
Subject: [PATCH] Version without type check and updated Article.thy

---
 Isa_DOF.thy                    |  4 ++--
 examples/simple/Article.thy    | 20 ++++++++++++--------
 ontologies/scholarly_paper.thy |  2 +-
 3 files changed, 15 insertions(+), 11 deletions(-)

diff --git a/Isa_DOF.thy b/Isa_DOF.thy
index df06f8f..da2569f 100644
--- a/Isa_DOF.thy
+++ b/Isa_DOF.thy
@@ -442,7 +442,7 @@ fun enriched_document_command markdown (((((oid,pos),cid_pos),
               val assns = map read_assn doc_attrs
               val _ = (SPY:=assns)       
               val defaults = base       (* this calculation ignores the defaults *)
-              val value_term = (fold convert assns defaults) |> (Sign.cert_term thy)
+              val value_term = (fold convert assns defaults) (* |> (Sign.cert_term thy) *)
               val name = Context.theory_name thy 
           in  thy |> DOF_core.define_object_global (oid, {pos=pos, 
                                                           thy_name=name,
@@ -476,7 +476,7 @@ fun update_instance_command  (((oid:string,pos),cid_pos),
                  (* Missing: Check that attributes are legal here *)
                  val assns = map read_assn doc_attrs
                  val _ = (SPY:=assns) 
-          in  thy |> DOF_core.update_value_global oid ((fold convert assns) #> (Sign.cert_term thy))
+          in  thy |> DOF_core.update_value_global oid ((fold convert assns) (* #> (Sign.cert_term thy) *))
           end
      in  Toplevel.theory(upd)
      end
diff --git a/examples/simple/Article.thy b/examples/simple/Article.thy
index ecefab4..662ccf3 100644
--- a/examples/simple/Article.thy
+++ b/examples/simple/Article.thy
@@ -11,10 +11,12 @@ text*[tit::title]{* Using The Isabelle Ontology Framework*}
 text*[stit::subtitle] \<open>Linking the Formal with the Informal\<close>
   
 text*[auth1::author, affiliation="''University of Sheffield''"]\<open>Achim Brucker\<close>
+  
 text*[auth2::author, affiliation="''Centrale-Supelec''"]       \<open>Idir Ait-Sadoune\<close>
 text*[auth3::author, affiliation="''IRT-SystemX''"]            \<open>Paolo Crisafulli\<close>
 text*[auth4::author, affiliation="''Universit\\'e Paris-Sud''"]\<open>Burkhart Wolff\<close>  
-  
+
+term "affiliation_update (\<lambda> _ . '''') S"  
   
 text*[abs::abstract, keyword_list="[]"] {* Isabelle/Isar is a system 
 framework with many similarities to Eclipse; it is mostly known as part of 
@@ -53,7 +55,7 @@ val (cid,value) = case DOF_core.get_object_global oid thy of
 
 val term'' = @{docitem_value \<open>bgrnd\<close>};
 
-val term' = Sign.certify_term @{theory} value;
+(* val term' = Sign.certify_term @{theory} value; *)
 simplify;
  *}  
   
@@ -72,20 +74,22 @@ val converts = fold convert (!AnnoTextelemParser.SPY) base
 
 
   
-term "\<lparr>author.tag_attribute=undefined,affiliation=undefined\<rparr>"
+term "\<lparr>author.tag_attribute=undefined,email=''dfg'',orcid=None,affiliation=undefined\<rparr>"
   
 ML{* !AnnoTextelemParser.SPY *}
 definition HURX where "HURX = affiliation((undefined::author)\<lparr>affiliation:='' ''\<rparr>)"
 thm HURX_def[simplified]
-ML{* 
+(*ML{* 
 val x = @{code "HURX"}
 *}
+*)
   
-definition HORX where "HORX = affiliation(\<lparr>author.tag_attribute=0,affiliation=''''\<rparr>\<lparr>affiliation:=''e''\<rparr>) "  
-ML{* 
+definition HORX 
+  where "HORX = affiliation(\<lparr>author.tag_attribute=undefined,email=''dfg'',orcid=None,affiliation=undefined\<rparr>\<lparr>affiliation:=''e''\<rparr>) "  
+(* ML{* 
 val x = @{code "HORX"}
 *}
-  
+*)  
   
 
   
@@ -93,7 +97,7 @@ term related_work.main_author_update
 section*[ontomod::technical]{* Modeling Ontologies in Isabelle_DOF *} 
 text{* Lorem ipsum dolor sit amet, suspendisse non arcu malesuada mollis, nibh morbi,*}
   
-text*[x]{* @{technical \<open>ontomod\<close>} @{technical \<open>bgrnd\<close>}*}
+text*[x]{* @{technical \<open>ontomod\<close>} @{introduction \<open>bgrnd\<close>}*}
   
 subsection*[scholar_onto::example]{* A Scholar Paper: Eating one's own dogfood. @{technical \<open>ontomod\<close>} *}  
 text{* @{technical \<open>ontomod\<close>}*}                                                
diff --git a/ontologies/scholarly_paper.thy b/ontologies/scholarly_paper.thy
index 647de1a..7125d8a 100644
--- a/ontologies/scholarly_paper.thy
+++ b/ontologies/scholarly_paper.thy
@@ -18,7 +18,7 @@ doc_class author =
    affiliation :: "string"
 
 doc_class abstract =
-   keyword_list :: "string list"  <= "[]"
+   keyword_list :: "string list"   <= "[]"
 
 
 doc_class text_section =