From a332109dca36243ac2066ae37c436205009d2d85 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Mon, 14 Mar 2022 15:27:13 +0100 Subject: [PATCH] Fix scheduling problem for term* and value* Toplevel transition only allows atomic transactions. So we avoid sequantial combinators --- src/DOF/Isa_DOF.thy | 41 +++++++++++++++++++++-------------------- 1 file changed, 21 insertions(+), 20 deletions(-) diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index 890628bd..c1995625 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -1746,7 +1746,8 @@ signature VALUE_COMMAND = sig val value: Proof.context -> term -> term val value_select: string -> Proof.context -> term -> term - val value_cmd: xstring -> string list -> string -> Toplevel.state -> Toplevel.transition -> unit + val value_cmd: (ODL_Command_Parser.meta_args_t option) -> xstring -> string list -> string + -> Toplevel.state -> Toplevel.transition -> unit val add_evaluator: binding * (Proof.context -> term -> term) -> theory -> string * theory end; @@ -1788,9 +1789,15 @@ fun value_select name ctxt = fun value ctxt term = value_select "" ctxt (DOF_core.transduce_term_global {mk_elaboration=true} (term , \<^here>) (Proof_Context.theory_of ctxt)) +fun meta_args_exec NONE thy = thy + |meta_args_exec (SOME ((((oid,pos),cid_pos), doc_attrs) : ODL_Command_Parser.meta_args_t)) thy = + thy |> (ODL_Command_Parser.create_and_check_docitem + {is_monitor = false} {is_inline = false} + oid pos (I cid_pos) (I doc_attrs)) -fun value_cmd raw_name modes raw_t state trans = +fun value_cmd meta_args_opt raw_name modes raw_t state trans = let + val _ = meta_args_exec meta_args_opt val ctxt = Toplevel.context_of state; val name = intern_evaluator ctxt raw_name; val t = Syntax.read_term ctxt raw_t; @@ -1817,22 +1824,17 @@ val opt_evaluator = val opt_attributes = Scan.option ODL_Command_Parser.attributes -fun meta_args_exec NONE thy = thy - |meta_args_exec (SOME ((((oid,pos),cid_pos), doc_attrs) : ODL_Command_Parser.meta_args_t)) thy = - thy |> (ODL_Command_Parser.create_and_check_docitem - {is_monitor = false} {is_inline = false} - oid pos (I cid_pos) (I doc_attrs)) - -fun pass_trans_to_value_cmd ((name, modes), t) trans = - Toplevel.keep (fn state => value_cmd name modes t state trans) trans +fun pass_trans_to_value_cmd meta_args_opt ((name, modes), t) trans = + Toplevel.keep (fn state => value_cmd meta_args_opt name modes t state trans) trans (* term* command uses the same code as term command and adds the possibility to check Term Annotation Antiquotations (TA) with the help of DOF_core.transduce_term_global function *) -fun string_of_term ctxt s trans = +fun string_of_term meta_args_opt ctxt s trans = let + val _ = meta_args_exec meta_args_opt val t = Syntax.read_term ctxt s; val T = Term.type_of t; val ctxt' = Proof_Context.augment t ctxt; @@ -1851,25 +1853,24 @@ Print_Mode.with_modes modes (fn () => writeln (string_of state arg)) ()); We want to have the current position to pass it to transduce_term_global in string_of_term, so we pass the Toplevel.transition *) -fun print_term (string_list, string) trans = print_item - (fn state => fn string => string_of_term (Toplevel.context_of state) string trans) - (string_list, string) trans; +fun print_term meta_args_opt (string_list, string) trans = print_item + (fn state => + fn string => + string_of_term meta_args_opt (Toplevel.context_of state) string trans) + (string_list, string) trans; val _ = Outer_Syntax.command \<^command_keyword>\term*\ "read and print term" (opt_attributes -- (opt_modes -- Parse.term) - >> (fn (meta_args_opt, eval_args ) => - Toplevel.theory (meta_args_exec meta_args_opt) - #> - print_term eval_args)); + >> (fn (meta_args_opt, eval_args ) => print_term meta_args_opt eval_args)); val _ = Outer_Syntax.command \<^command_keyword>\value*\ "evaluate and print term" (opt_attributes -- (opt_evaluator -- opt_modes -- Parse.term) - >> (fn (meta_args_opt, eval_args ) => + >> (fn (meta_args_opt, eval_args ) => Toplevel.theory (meta_args_exec meta_args_opt) #> - pass_trans_to_value_cmd eval_args)); + pass_trans_to_value_cmd meta_args_opt eval_args)); val _ = Theory.setup (Thy_Output.antiquotation_pretty_source_embedded \<^binding>\value*\