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

Cleanup and add position to docitem ML antiqutation
ci/woodpecker/push/build Pipeline failed Details

This commit is contained in:
Nicolas Méric 2023-01-26 09:43:51 +01:00
parent 20b0af740d
commit ba8227e6ab
1 changed files with 7 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
src/DOF/Isa_DOF.thy
View File

@ -2524,16 +2524,15 @@ fun attr_2_ML ctxt ((attr:string,pos),(oid:string,pos')) = (ML_Syntax.atomic o M
(ISA_core.compute_attr_access ctxt attr oid (SOME 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
let val ctxt' = Context.the_proof ctxt
val value = case DOF_core.get_object_local oid ctxt' of
SOME({pos=pos_decl,id,value,...}) =>
let val markup = docref_markup false oid id pos_decl
val _ = Context_Position.report ctxt' pos markup
in value end
| NONE => error "not an object id"
val _ = (TERM_STORE := term) (* export to the ML Context *)
in "! AttributeAccess.TERM_STORE" end
in ML_Syntax.print_term value 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