Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Version without type check and updated Article.thy

This commit is contained in:
Burkhart Wolff 2018-04-27 12:05:22 +02:00
parent 5bcd4c19b1
commit f01b36997e
3 changed files with 15 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
Isa_DOF.thy
View File

@ -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

20
examples/simple/Article.thy
View File

@ -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>}*}

2
ontologies/scholarly_paper.thy
View File

@ -18,7 +18,7 @@ doc_class author =
affiliation :: "string"
doc_class abstract =
keyword_list :: "string list" <= "[]"
keyword_list :: "string list" <= "[]"
doc_class text_section =