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

Use name spaced names for docitem_name text anti-quotation

This commit is contained in:
Nicolas Méric 2024-03-12 18:21:53 +01:00
parent 10b98b660f
commit 291b2e258f
1 changed files with 11 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

21
Isabelle_DOF/thys/Isa_DOF.thy
View File

@ -2910,6 +2910,7 @@ fun compute_trace_ML ctxt oid pos_opt pos' =
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_oid'' = Scan.lift(Parse.embedded_position)
val parse_cid' = Term_Style.parse -- parse_cid
@ -2954,13 +2955,6 @@ fun compute_cid_repr ctxt cid _ =
let val _ = DOF_core.get_onto_class_name_global cid (Proof_Context.theory_of ctxt)
in Const(cid,dummyT) end
fun compute_name_repr ctxt oid pos =
let val instances = DOF_core.get_instances ctxt
val markup = DOF_core.get_instance_name_global oid (Proof_Context.theory_of ctxt)
|> Name_Space.markup (Name_Space.space_of_table instances)
val _ = Context_Position.report ctxt pos markup;
in HOLogic.mk_string oid end
local
fun pretty_attr_access_style ctxt (style, ((attr,pos),(oid,pos'))) =
@ -2970,8 +2964,15 @@ fun pretty_trace_style ctxt (style, (oid,pos)) =
Document_Output.pretty_term ctxt (style (ISA_core.compute_attr_access (Context.Proof ctxt)
traceN oid NONE pos));
fun pretty_name_style ctxt (style, (oid,pos)) =
Document_Output.pretty_term ctxt (style (compute_name_repr ctxt oid pos))
fun pretty_name_style ctxt (oid,pos) =
let
val instances = DOF_core.get_instances ctxt
val ns = Name_Space.space_of_table instances
val name = DOF_core.get_instance_name_global oid (Proof_Context.theory_of ctxt)
val ctxt' = Config.put Name_Space.names_unique true ctxt
val _ = name |> Name_Space.markup ns
|> Context_Position.report ctxt pos
in Name_Space.pretty ctxt' ns name end
fun pretty_cid_style ctxt (style, (cid,pos)) =
Document_Output.pretty_term ctxt (style (compute_cid_repr ctxt cid pos));
@ -3009,7 +3010,7 @@ val _ = Theory.setup
basic_entity \<^binding>\<open>doc_class\<close> parse_cid' pretty_cid_style #>
basic_entity \<^binding>\<open>onto_class\<close> parse_cid' pretty_cid_style #>
basic_entity \<^binding>\<open>docitem_attribute\<close> parse_attribute_access' pretty_attr_access_style #>
basic_entity \<^binding>\<open>docitem_name\<close> parse_oid' pretty_name_style
basic_entity \<^binding>\<open>docitem_name\<close> parse_oid'' pretty_name_style
)
end
end