# HG changeset patch # User wenzelm # Date 1742592378 -3600 # Node ID 231b6d8231c6a66e0152dcf493bcda073c8fc3e4 # Parent 83584916b6d7e42a24dddadba15b37486185e1e7 more uniform Proof_Display.print_results for theory and proof output --- avoid loss of information seen in src/Doc/JEdit/document/output-and-state.png (the first bad changeset is f8c412a45af8, see also 53b59fa42696); diff -r 83584916b6d7 -r 231b6d8231c6 NEWS --- a/NEWS Fri Mar 21 18:37:05 2025 +0100 +++ b/NEWS Fri Mar 21 22:26:18 2025 +0100 @@ -7,6 +7,16 @@ New in this Isabelle version ---------------------------- +*** General *** + +* Isar proof results --- notably from finished 'have' or 'show' --- are +printed as regular "writeln" message instead of "state": this follows +toplevel results from Isabelle2023. The order of output messages has +been fine-tuned accordingly, to show results as "urgent" message before +state output (if enabled). This affects Isabelle/jEdit panels for Output +vs. State in particular. + + *** HOL *** * Theory "HOL.Fun": diff -r 83584916b6d7 -r 231b6d8231c6 src/HOL/Library/simps_case_conv.ML --- a/src/HOL/Library/simps_case_conv.ML Fri Mar 21 18:37:05 2025 +0100 +++ b/src/HOL/Library/simps_case_conv.ML Fri Mar 21 22:26:18 2025 +0100 @@ -117,8 +117,7 @@ val thm = Attrib.eval_thms lthy thms_ref |> to_case lthy val (res, lthy') = Local_Theory.note (bind', [thm]) lthy val _ = - Proof_Display.print_results - {interactive = int, pos = Position.thread_data (), proof_state = false} + Proof_Display.print_results {interactive = int, pos = Position.thread_data ()} lthy' ((Thm.theoremK, ""), [res]) in lthy' end @@ -131,8 +130,7 @@ else gen_to_simps lthy (Attrib.eval_thms lthy splits_ref) thm val (res, lthy') = Local_Theory.note (bind', simps) lthy val _ = - Proof_Display.print_results - {interactive = int, pos = Position.thread_data (), proof_state = false} + Proof_Display.print_results {interactive = int, pos = Position.thread_data ()} lthy' ((Thm.theoremK, ""), [res]) in lthy' end diff -r 83584916b6d7 -r 231b6d8231c6 src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Fri Mar 21 18:37:05 2025 +0100 +++ b/src/HOL/Tools/inductive.ML Fri Mar 21 22:26:18 2025 +0100 @@ -617,8 +617,7 @@ args thmss; val (res, lthy') = lthy |> Local_Theory.notes facts val _ = - Proof_Display.print_results - {interactive = int, pos = Position.thread_data (), proof_state = false} + Proof_Display.print_results {interactive = int, pos = Position.thread_data ()} lthy' ((Thm.theoremK, ""), res); in (res, lthy') end; @@ -680,8 +679,7 @@ map (Thm.no_attributes o single o mk_simp_eq lthy o prep_prop lthy) props)); val (res, lthy') = lthy |> Local_Theory.notes facts val _ = - Proof_Display.print_results - {interactive = int, pos = Position.thread_data (), proof_state = false} + Proof_Display.print_results {interactive = int, pos = Position.thread_data ()} lthy' ((Thm.theoremK, ""), res) in (res, lthy') end; diff -r 83584916b6d7 -r 231b6d8231c6 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Fri Mar 21 18:37:05 2025 +0100 +++ b/src/Pure/Isar/proof.ML Fri Mar 21 22:26:18 2025 +0100 @@ -1231,8 +1231,7 @@ fun gen_have prep_statement prep_att strict_asm before_qed after_qed fixes assumes shows int = local_goal - (Proof_Display.print_results - {interactive = int, pos = Position.thread_data (), proof_state = true}) + (Proof_Display.print_results {interactive = int, pos = Position.thread_data ()}) prep_statement prep_att strict_asm "have" before_qed after_qed fixes assumes shows; fun gen_show prep_statement prep_att strict_asm before_qed after_qed fixes assumes shows int state = @@ -1244,16 +1243,15 @@ (case ! rule of NONE => [] | SOME th => [Proof_Display.string_of_rule ctxt "Failed" th]) |> cat_lines; - val pos = Position.thread_data (); fun print_results ctxt res = if ! testing then () - else Proof_Display.print_results {interactive = int, pos = pos, proof_state = true} ctxt res; + else Proof_Display.print_results {interactive = int, pos = Position.thread_data ()} ctxt res; fun print_rule ctxt th = if ! testing then rule := SOME th else if int then Proof_Display.string_of_rule ctxt "Successful" th |> Markup.markup Markup.text_fold - |> Output.state + |> Output.writeln_urgent else (); val test_proof = local_skip_proof true diff -r 83584916b6d7 -r 231b6d8231c6 src/Pure/Isar/proof_display.ML --- a/src/Pure/Isar/proof_display.ML Fri Mar 21 18:37:05 2025 +0100 +++ b/src/Pure/Isar/proof_display.ML Fri Mar 21 22:26:18 2025 +0100 @@ -18,7 +18,7 @@ val method_error: string -> Position.T -> {context: Proof.context, facts: thm list, goal: thm} -> 'a Seq.result val show_results: bool Config.T - val print_results: {interactive: bool, pos: Position.T, proof_state: bool} -> Proof.context -> + val print_results: {interactive: bool, pos: Position.T} -> Proof.context -> ((string * string) * (string * thm list) list) -> unit val print_theorem: Position.T -> Proof.context -> string * thm list -> unit val print_consts: bool -> Position.T -> Proof.context -> @@ -317,25 +317,22 @@ in -fun print_results {interactive, pos, proof_state} ctxt ((kind, name), facts) = - let val print = if proof_state then Output.state o Pretty.string_of else Pretty.writeln in - if kind = "" orelse no_print interactive ctxt then () - else if name = "" then - print - (Pretty.block (Pretty.mark_position pos (Pretty.keyword1 kind) :: Pretty.brk 1 :: - pretty_facts ctxt facts)) - else - print - (case facts of - [fact] => Pretty.block1 [pretty_fact_name pos (kind, name), Pretty.fbrk, - Proof_Context.pretty_fact ctxt fact] - | _ => Pretty.block1 [pretty_fact_name pos (kind, name), Pretty.fbrk, - Pretty.block1 (Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]) - end; +fun print_results {interactive, pos} ctxt ((kind, name), facts) = + if kind = "" orelse no_print interactive ctxt then () + else if name = "" then + Pretty.writeln_urgent + (Pretty.block (Pretty.mark_position pos (Pretty.keyword1 kind) :: Pretty.brk 1 :: + pretty_facts ctxt facts)) + else + Pretty.writeln_urgent + (case facts of + [fact] => Pretty.block1 [pretty_fact_name pos (kind, name), Pretty.fbrk, + Proof_Context.pretty_fact ctxt fact] + | _ => Pretty.block1 [pretty_fact_name pos (kind, name), Pretty.fbrk, + Pretty.block1 (Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]); fun print_theorem pos ctxt fact = - print_results {interactive = true, pos = pos, proof_state = false} - ctxt ((Thm.theoremK, ""), [fact]); + print_results {interactive = true, pos = pos} ctxt ((Thm.theoremK, ""), [fact]); end; diff -r 83584916b6d7 -r 231b6d8231c6 src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Fri Mar 21 18:37:05 2025 +0100 +++ b/src/Pure/Isar/specification.ML Fri Mar 21 22:26:18 2025 +0100 @@ -344,8 +344,7 @@ |> Attrib.transform_facts (Proof_Context.export_morphism ctxt' lthy); val (res, lthy') = lthy |> Local_Theory.notes_kind kind facts'; val _ = - Proof_Display.print_results - {interactive = int, pos = Position.thread_data (), proof_state = false} + Proof_Display.print_results {interactive = int, pos = Position.thread_data ()} lthy' ((kind, ""), res); in (res, lthy') end; @@ -398,9 +397,8 @@ |> prep_statement (prep_att lthy) prep_stmt elems raw_concl; val atts = more_atts @ map (prep_att lthy) raw_atts; - val pos = Position.thread_data (); val print_results = - Proof_Display.print_results {interactive = int, pos = pos, proof_state = false}; + Proof_Display.print_results {interactive = int, pos = Position.thread_data ()}; fun after_qed' results goal_ctxt' = let diff -r 83584916b6d7 -r 231b6d8231c6 src/Pure/ex/Guess.thy --- a/src/Pure/ex/Guess.thy Fri Mar 21 18:37:05 2025 +0100 +++ b/src/Pure/ex/Guess.thy Fri Mar 21 22:26:18 2025 +0100 @@ -147,9 +147,8 @@ val guess = (("guess", 0), propT); val goal = Var guess; - val pos = Position.thread_data (); fun print_result ctxt' (k, [(s, [_, th])]) = - Proof_Display.print_results {interactive = int, pos = pos, proof_state = true} + Proof_Display.print_results {interactive = int, pos = Position.thread_data ()} ctxt' (k, [(s, [th])]); val before_qed = Method.primitive_text (fn ctxt =>