# 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 =>