nicolas.meric
/
Isabelle_DOF
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Disable invariants checking for declare_reference* without meta args

This commit is contained in:
Nicolas Méric 2023-03-13 11:31:48 +01:00
parent 37afd975b3
commit dde865520a
1 changed files with 18 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

31
Isabelle_DOF/thys/Isa_DOF.thy
View File

@ -1780,19 +1780,24 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} {define=define} oi
|> value (Proof_Context.init_global thy), |> value (Proof_Context.init_global thy),
is_inline, cid_long, vcid)) is_inline, cid_long, vcid))
|> register_oid_cid_in_open_monitors oid pos cid_pos' |> register_oid_cid_in_open_monitors oid pos cid_pos'
|> tap (DOF_core.check_opening_ml_invs cid_long oid is_monitor) |> (fn thy =>
|> tap (DOF_core.check_ml_invs cid_long oid is_monitor) if (* declare_reference* without arguments is not checked against invariants *)
(* Bypass checking of high-level invariants when the class default_cid = "text", thy |> DOF_core.get_defined_global oid |> not
the top (default) document class. andalso null doc_attrs
We want the class default_cid to stay abstract then thy
and not have the capability to be defined with attribute, invariants, etc. else thy |> tap (DOF_core.check_opening_ml_invs cid_long oid is_monitor)
Hence this bypass handles docitem without a class associated, |> tap (DOF_core.check_ml_invs cid_long oid is_monitor)
for example when you just want a document element to be referenceable (* Bypass checking of high-level invariants when the class default_cid = "text",
without using the burden of ontology classes. the top (default) document class.
ex: text*[sdf]\<open> Lorem ipsum @{thm refl}\<close> *) We want the class default_cid to stay abstract
|> (fn thy => if default_cid then thy and not have the capability to be defined with attribute, invariants, etc.
else if Config.get_global thy DOF_core.invariants_checking Hence this bypass handles docitem without a class associated,
then check_invariants thy (oid, pos) else thy) for example when you just want a document element to be referenceable
without using the burden of ontology classes.
ex: text*[sdf]\<open> Lorem ipsum @{thm refl}\<close> *)
|> (fn thy => if default_cid then thy
else if Config.get_global thy DOF_core.invariants_checking
then check_invariants thy (oid, pos) else thy))
end end
end (* structure Docitem_Parser *) end (* structure Docitem_Parser *)