diff --git a/Isabelle_DOF-Unit-Tests/TestKit.thy b/Isabelle_DOF-Unit-Tests/TestKit.thy index fa8d468b..34c5abf7 100644 --- a/Isabelle_DOF-Unit-Tests/TestKit.thy +++ b/Isabelle_DOF-Unit-Tests/TestKit.thy @@ -152,10 +152,10 @@ val _ = val _ = - let fun pass_trans_to_value_cmd (args, (((name, modes), t),src)) trans = - (Value_Command.value_cmd {assert=false} args name modes t @{here} trans + let fun pass_trans_to_value_cmd (args, (((name, modes), t),src)) thy = + (Value_Command.value_cmd' {assert=false} args name modes t @{here} thy handle ERROR msg => (if error_match src msg - then (writeln ("Correct error: "^msg^": reported.");trans) + then (writeln ("Correct error: "^msg^": reported.");thy) else error"Wrong error reported")) in Outer_Syntax.command \<^command_keyword>\value-assert-error\ "evaluate and print term" (ODL_Meta_Args_Parser.opt_attributes -- diff --git a/Isabelle_DOF/thys/Isa_DOF.thy b/Isabelle_DOF/thys/Isa_DOF.thy index c3209403..b1b26858 100644 --- a/Isabelle_DOF/thys/Isa_DOF.thy +++ b/Isabelle_DOF/thys/Isa_DOF.thy @@ -1837,31 +1837,36 @@ fun meta_args_exec (meta_args as (((oid, pos), cid_pos), doc_attrs) : ODL_Meta_A {is_monitor = false} {is_inline = true} {define = true} oid pos (I cid_pos) (I doc_attrs)) -fun value_cmd {assert=assert} meta_args_opt raw_name modes raw_t pos thy = - let - val thy' = meta_args_exec meta_args_opt thy - val name = intern_evaluator thy' raw_name; - val t = Syntax.read_term_global thy' raw_t; - val term' = DOF_core.transduce_term_global {mk_elaboration=true} (t , pos) - (thy'); - val t' = value_select name (Proof_Context.init_global thy') term'; - val ty' = Term.type_of t'; - val ty' = if assert - then case ty' of - \<^typ>\bool\ => ty' - | _ => error "Assertion expressions must be boolean." - else ty' - val t' = if assert - then case t' of - \<^term>\True\ => t' - | _ => error "Assertion failed." - else t' - val ctxt' = Proof_Context.augment t' (Proof_Context.init_global thy'); - val p = Print_Mode.with_modes modes (fn () => - Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk, - Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) (); - val _ = Pretty.writeln p - in thy' end; +fun value_cmd {assert=assert} raw_name modes raw_t pos state = +let + val thy' = Toplevel.theory_of state; + val name = intern_evaluator thy' raw_name; + val t = Syntax.read_term_global thy' raw_t; + val term' = DOF_core.transduce_term_global {mk_elaboration=true} (t , pos) + (thy'); + val t' = value_select name (Proof_Context.init_global thy') term'; + val ty' = Term.type_of t'; + val ty' = if assert + then case ty' of + \<^typ>\bool\ => ty' + | _ => error "Assertion expressions must be boolean." + else ty' + val t'' = if assert + then case t' of + \<^term>\True\ => t' + | _ => error "Assertion failed." + else t' + val ctxt' = Proof_Context.augment t'' (Proof_Context.init_global thy'); + val p = Print_Mode.with_modes modes (fn () => + Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t''), Pretty.fbrk, + Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) (); +in Pretty.writeln p end; + +fun value_cmd' assert meta_args_opt raw_name modes raw_t pos thy = +let + val thy' = meta_args_exec meta_args_opt thy + val _ = value_cmd assert raw_name modes raw_t pos (Toplevel.theory_toplevel thy') +in thy' end; val opt_modes = Scan.optional (\<^keyword>\(\ |-- Parse.!!! (Scan.repeat1 Parse.name --| \<^keyword>\)\)) []; @@ -1871,8 +1876,9 @@ val opt_evaluator = fun pass_trans_to_value_cmd meta_args_opt ((name, modes), t) trans = let val pos = Toplevel.pos_of trans -in - trans |> Toplevel.theory (value_cmd {assert=false} meta_args_opt name modes t pos) +in if meta_args_opt = ODL_Meta_Args_Parser.empty_meta_args + then trans |> Toplevel.keep (value_cmd {assert=false} name modes t pos) + else trans |> Toplevel.theory (value_cmd' {assert=false} meta_args_opt name modes t pos) end \ \c.f. \<^file>\~~/src/Pure/Isar/isar_cmd.ML\\ @@ -1882,7 +1888,7 @@ end and adds the possibility to check Term Annotation Antiquotations (TA) with the help of DOF_core.transduce_term_global function *) -fun string_of_term s pos ctxt = +fun string_of_term ctxt pos s = let val t = Syntax.read_term ctxt s; val T = Term.type_of t; @@ -1898,14 +1904,16 @@ end; fun print_item string_of (modes, arg) state = Print_Mode.with_modes modes (fn () => writeln (string_of state arg)) (); -fun prin t pos state _ = string_of_term t pos (Toplevel.context_of state) +fun prin s pos state _ = string_of_term (Toplevel.context_of state) pos s fun print_term meta_args_opt (string_list, string) trans = let val pos = Toplevel.pos_of trans -in meta_args_exec meta_args_opt - #> tap (fn thy => print_item (prin string pos) (string_list, string) (Toplevel.theory_toplevel thy)) - |> (fn thy => Toplevel.theory thy trans) +in if meta_args_opt = ODL_Meta_Args_Parser.empty_meta_args + then Toplevel.keep (print_item (prin string pos) (string_list, string)) trans + else meta_args_exec meta_args_opt + #> tap (fn thy => print_item (prin string pos) (string_list, string) (Toplevel.theory_toplevel thy)) + |> (fn thy => Toplevel.theory thy trans) end val (disable_assert_evaluation, disable_assert_evaluation_setup) @@ -1915,14 +1923,20 @@ val _ = Theory.setup disable_assert_evaluation_setup fun pass_trans_to_assert_value_cmd meta_args_opt ((name, modes), t) trans = let val pos = Toplevel.pos_of trans -in trans - |> Toplevel.theory - (fn thy => - if Config.get_global thy disable_assert_evaluation - then (meta_args_exec meta_args_opt - #> tap (fn thy => print_item (prin t pos) (modes, t) (Toplevel.theory_toplevel thy))) - thy - else value_cmd {assert=true} meta_args_opt name modes t pos thy) +in if meta_args_opt = ODL_Meta_Args_Parser.empty_meta_args + then trans |> Toplevel.keep + (fn state => + let val thy = Toplevel.theory_of state + in if Config.get_global thy disable_assert_evaluation + then print_item (prin t pos) (modes, t) state + else value_cmd {assert=true} name modes t pos state end) + else trans |> Toplevel.theory + (fn thy => + if Config.get_global thy disable_assert_evaluation + then thy |> (meta_args_exec meta_args_opt + #> tap (fn thy => (Toplevel.theory_toplevel thy) + |> print_item (prin t pos) (modes, t))) + else (value_cmd' {assert=true} meta_args_opt name modes t pos) thy) end (* setup ontology aware commands *)