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

Fix declare_reference behavior
ci/woodpecker/push/build Pipeline failed Details 

- Fix "unchecked" text onto_class antiqutation option
- Update text-assert-error function to make meta-arguments optional
This commit is contained in:
Nicolas Méric 2023-03-06 12:20:58 +01:00
parent ef8ffda414
commit 10b90c823f
3 changed files with 32 additions and 19 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
Isabelle_DOF-Unit-Tests/Concept_OntoReferencing.thy
View File

@ -65,9 +65,9 @@ text-assert-error[ae1]\<open>@{C \<open>c1\<close>}\<close>\<open>Undefined inst
declare_reference*[c1::C] \<comment> \<open>forward declaration\<close>
text\<open>@{C \<open>c1\<close>} \<close> \<comment> \<open>THIS IS A BUG !!! OVERLY SIMPLISTIC BEHAVIOUR. THIS SHOULD FAIL! \<close>
text-assert-error\<open>@{C \<open>c1\<close>} \<close>\<open>Instance declared but not defined, try option unchecked\<close>
text\<open>@{C (unchecked) \<open>c1\<close>} \<close> \<comment> \<open>THIS SHOULD BE THE CORRECT BEHAVIOUR! \<close>
text\<open>@{C (unchecked) \<open>c1\<close>} \<close>
text*[c1::C, x = "''beta''"] \<open> ... suspendisse non arcu malesuada mollis, nibh morbi, ... \<close>

27
Isabelle_DOF-Unit-Tests/TestKit.thy
View File

@ -29,12 +29,15 @@ section\<open>Testing Commands (exec-catch-verify - versions of std commands)\<c
ML\<open>
fun gen_enriched_document_command2 name {body} cid_transform attr_transform markdown
(((((oid,pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t,
((meta_args,
xstring_opt:(xstring * Position.T) option),
toks_list:Input.source list)
: theory -> theory =
let val toplvl = Toplevel.theory_toplevel
val (((oid,pos),cid_pos), doc_attrs) = meta_args
val oid' = if meta_args = ODL_Meta_Args_Parser.empty_meta_args
then "output"
else oid
(* as side-effect, generates markup *)
fun check_n_tex_text thy toks = let val ctxt = Toplevel.presentation_context (toplvl thy);
val pos = Input.pos_of toks;
@ -52,7 +55,7 @@ fun gen_enriched_document_command2 name {body} cid_transform attr_transform mark
(* type file = {path: Path.T, pos: Position.T, content: string} *)
val strg = XML.string_of (hd (Latex.output text))
val file = {path = Path.make [oid ^ "_snippet.tex"],
val file = {path = Path.make [oid' ^ "_snippet.tex"],
pos = @{here},
content = Bytes.string strg}
@ -66,10 +69,13 @@ fun gen_enriched_document_command2 name {body} cid_transform attr_transform mark
(* ... generating the level-attribute syntax *)
in
( Value_Command.Docitem_Parser.create_and_check_docitem
(if meta_args = ODL_Meta_Args_Parser.empty_meta_args
then I
else
Value_Command.Docitem_Parser.create_and_check_docitem
{is_monitor = false} {is_inline = false} {define = true}
oid pos (cid_transform cid_pos) (attr_transform doc_attrs)
#> (fn thy => (app (check_n_tex_text thy) toks_list; thy)))
oid pos (cid_transform cid_pos) (attr_transform doc_attrs))
#> (fn thy => (app (check_n_tex_text thy) toks_list; thy))
end;
val _ =
@ -117,10 +123,11 @@ fun error_match2 [_, src] msg = error_match src msg
val _ =
Outer_Syntax.command ("text-assert-error", @{here}) "formal comment macro"
(ODL_Meta_Args_Parser.attributes -- Parse.opt_target -- Scan.repeat1 Parse.document_source
>> (Toplevel.theory o (gen_enriched_document_command3 error_match2 "TTT" {body=true}
I I {markdown = true})
));
(ODL_Meta_Args_Parser.opt_attributes -- Parse.opt_target -- Scan.repeat1 Parse.document_source
>> (Toplevel.theory o
(fn ((meta_args, xstring_opt), source) =>
(gen_enriched_document_command3 error_match2 "TTT" {body=true}
I I {markdown = true} ((meta_args, xstring_opt), source)))));
fun update_instance_command (args,src) thy =
(Monitor_Command_Parser.update_instance_command args thy

20
Isabelle_DOF/thys/Isa_DOF.thy
View File

@ -1791,10 +1791,9 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} {define=define} oi
end (* structure Docitem_Parser *)
val empty_meta_args = ((("", Position.none), NONE), [])
fun meta_args_exec (meta_args as (((oid, pos), cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) thy =
thy |> (if meta_args = empty_meta_args
thy |> (if meta_args = ODL_Meta_Args_Parser.empty_meta_args
then (K thy)
else Docitem_Parser.create_and_check_docitem
{is_monitor = false} {is_inline = false} {define = true}
@ -2297,9 +2296,9 @@ ML\<open>
structure ML_star_Command =
struct
fun meta_args_exec (meta_args as (((oid, pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) thy =
thy |> (if meta_args = Value_Command.empty_meta_args
then (K thy)
fun meta_args_exec (meta_args as (((oid, pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) ctxt =
ctxt |> (if meta_args = ODL_Meta_Args_Parser.empty_meta_args
then (K ctxt)
else Context.map_theory (Value_Command.Docitem_Parser.create_and_check_docitem
{is_monitor = false} {is_inline = false}
{define = true} oid pos (I cid_pos) (I doc_attrs))
@ -2661,10 +2660,17 @@ struct
val basic_entity = Document_Output.antiquotation_pretty_source
: binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory;
fun check_and_mark ctxt cid_decl (str:{strict_checking: bool}) {inline=inline_req} pos name =
fun check_and_mark ctxt cid_decl ({strict_checking = strict}) {inline=inline_req} pos name =
let
val thy = Proof_Context.theory_of ctxt;
val DOF_core.Instance {cid,inline,...} = DOF_core.get_instance_global name thy
val DOF_core.Instance {cid,inline, defined, ...} = DOF_core.get_instance_global name thy
val _ = if not strict
then if defined
then ISA_core.warn ("Instance defined, unchecked option useless") pos
else ()
else if defined
then ()
else ISA_core.err ("Instance declared but not defined, try option unchecked") pos
val _ = if not inline_req
then if inline then () else error("referred text-element is macro! (try option display)")
else if not inline then () else error("referred text-element is no macro!")