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

addded docitem ML antiquotation. (Kleine Fingeruebung).

This commit is contained in:
Burkhart Wolff 2021-04-21 20:24:06 +02:00
parent 0b6ef076b0
commit 3b21df199b
3 changed files with 22 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
src/DOF/Isa_DOF.thy
View File

@ -1647,8 +1647,8 @@ fun compute_trace_ML ctxt oid pos pos' =
fun conv (Const(@{const_name "Pair"},_) $ Const(s,_) $ S) = (s, HOLogic.dest_string S)
in map conv (HOLogic.dest_list term) end
val parse_oid = Scan.lift(Parse.position Args.name)
val parse_cid = Scan.lift(Parse.position Args.name)
val parse_oid = Scan.lift(Parse.position Args.name)
val parse_cid = Scan.lift(Parse.position Args.name)
val parse_oid' = Term_Style.parse -- parse_oid
val parse_cid' = Term_Style.parse -- parse_cid
@ -1664,6 +1664,18 @@ val parse_attribute_access' = Term_Style.parse -- parse_attribute_access
fun attr_2_ML ctxt ((attr:string,pos),(oid:string,pos')) = (ML_Syntax.atomic o ML_Syntax.print_term)
(compute_attr_access ctxt attr oid pos pos')
val TERM_STORE = let val dummy_term = Bound 0
in Unsynchronized.ref (dummy_term) end
fun get_instance_value_2_ML ctxt (oid:string,pos) =
let val term = case DOF_core.get_value_global oid (Context.theory_of ctxt) of
SOME(t) => t
| NONE => error "not an object id"
val _ = (TERM_STORE := term) (* export to the ML Context *)
in "! AttributeAccess.TERM_STORE" end
fun trace_attr_2_ML ctxt (oid:string,pos) =
let val print_string_pair = ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_string
val toML = (ML_Syntax.atomic o (ML_Syntax.print_list print_string_pair))
@ -1686,7 +1698,9 @@ fun pretty_cid_style ctxt (style, (cid,pos)) =
in
val _ = Theory.setup
(ML_Antiquotation.inline \<^binding>\<open>docitem_attribute\<close>
(ML_Antiquotation.inline \<^binding>\<open>docitem\<close>
(fn (ctxt,toks) => (parse_oid >> get_instance_value_2_ML ctxt) (ctxt, toks)) #>
ML_Antiquotation.inline \<^binding>\<open>docitem_attribute\<close>
(fn (ctxt,toks) => (parse_attribute_access >> attr_2_ML ctxt) (ctxt, toks)) #>
ML_Antiquotation.inline \<^binding>\<open>trace_attribute\<close>
(fn (ctxt,toks) => (parse_oid >> trace_attr_2_ML ctxt) (ctxt, toks)) #>

3
src/ontologies/Conceptual/Conceptual.thy
View File

@ -76,11 +76,12 @@ ML\<open> Session.get_keywords(); (* this looks to be really session global. *)
ML\<open> Thy_Header.get_keywords @{theory};(* this looks to be really theory global. *) \<close>
*)
open_monitor*[aaa::M]
section*[test::A]\<open>Test and Validation\<close>
text\<open>Defining some document elements to be referenced in later on in another theory: \<close>
text*[sdf]\<open> Lorem ipsum @{thm refl}\<close>
text*[ sdfg :: F] \<open> Lorem ipsum @{thm refl}\<close>
text*[ xxxy ] \<open> Lorem ipsum @{F \<open>sdfg\<close>} rate @{thm refl}\<close>
close_monitor*[aaa]
end

4
src/tests/TermAntiquotations.thy
View File

@ -79,8 +79,10 @@ a @{typ "C"}-type is required, but a @{typ "G"}-type is offered which is legal
\verb+Isa_DOF+ because of the sub-class relation between those classes: \<close>
update_instance*[xcv4::F, b+="{(@{docitem ''xcv3''},@{docitem ''xcv5''})}"]
text\<open>And here is the result on term level:\<close>
text\<open>And here is the results of some ML-term antiquotations:\<close>
ML\<open> @{docitem_attribute b::xcv4} \<close>
ML\<open> @{docitem xcv4} \<close>
ML\<open> @{trace_attribute aaa} \<close>
end