prefer Output.writeln for theory "results", as opposed to Output.state for genuine proof states (see f8c412a45af8, c668735fb8b5, ecf80e37ed1a);

--- a/NEWS	Wed Jul 26 15:42:13 2023 +0200
+++ b/NEWS	Wed Jul 26 20:15:31 2023 +0200
@@ -9,6 +9,11 @@
 
 *** General ***
 
+* Toplevel results --- like declared consts and proven theorems --- are
+printed as regular "writeln" message instead of "state", which is no
+specifically for proof states. This affects Isabelle/jEdit panels for
+Output vs. State in particular.
+
 * Session build dependencies (sources and heaps) are now recorded in
 more details, with one SHA1 digest per file and a symbolic version of
 the file name -- similar to the Unix command-line tool "sha1sum". For

--- a/src/Pure/Isar/proof.ML	Wed Jul 26 15:42:13 2023 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Jul 26 20:15:31 2023 +0200
@@ -1153,7 +1153,7 @@
     val _ =
       (case Proof_Display.pretty_goal_inst goal_ctxt propss goal of
         [] => ()
-      | prts => Output.state (Pretty.string_of (Pretty.chunks prts)));
+      | prts => Pretty.writeln (Pretty.chunks prts));
   in result_ctxt end;
 
 fun global_qed arg =
@@ -1231,7 +1231,9 @@
 local
 
 fun gen_have prep_statement prep_att strict_asm before_qed after_qed fixes assumes shows int =
-  local_goal (Proof_Display.print_results int (Position.thread_data ()))
+  local_goal
+    (Proof_Display.print_results
+      {interactive = int, pos = Position.thread_data (), proof_state = true})
     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 =
@@ -1246,7 +1248,7 @@
     val pos = Position.thread_data ();
     fun print_results ctxt res =
       if ! testing then ()
-      else Proof_Display.print_results int pos ctxt res;
+      else Proof_Display.print_results {interactive = int, pos = pos, proof_state = true} ctxt res;
     fun print_rule ctxt th =
       if ! testing then rule := SOME th
       else if int then

--- a/src/Pure/Isar/proof_display.ML	Wed Jul 26 15:42:13 2023 +0200
+++ b/src/Pure/Isar/proof_display.ML	Wed Jul 26 20:15:31 2023 +0200
@@ -24,7 +24,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: bool -> Position.T -> Proof.context ->
+  val print_results: {interactive: bool, pos: Position.T, proof_state: bool} -> 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 ->
@@ -349,22 +349,25 @@
 
 in
 
-fun print_results int pos ctxt ((kind, name), facts) =
-  if kind = "" orelse no_print int ctxt then ()
-  else if name = "" then
-    (Output.state o Pretty.string_of)
-      (Pretty.block (position_markup pos (Pretty.keyword1 kind) :: Pretty.brk 1 ::
-        pretty_facts ctxt facts))
-  else
-    (Output.state o Pretty.string_of)
-      (case facts of
-        [fact] => Pretty.blk (1, [pretty_fact_name pos (kind, name), Pretty.fbrk,
-          Proof_Context.pretty_fact ctxt fact])
-      | _ => Pretty.blk (1, [pretty_fact_name pos (kind, name), Pretty.fbrk,
-          Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]));
+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 (position_markup pos (Pretty.keyword1 kind) :: Pretty.brk 1 ::
+          pretty_facts ctxt facts))
+    else
+      print
+        (case facts of
+          [fact] => Pretty.blk (1, [pretty_fact_name pos (kind, name), Pretty.fbrk,
+            Proof_Context.pretty_fact ctxt fact])
+        | _ => Pretty.blk (1, [pretty_fact_name pos (kind, name), Pretty.fbrk,
+            Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]))
+  end;
 
 fun print_theorem pos ctxt fact =
-  print_results true pos ctxt ((Thm.theoremK, ""), [fact]);
+  print_results {interactive = true, pos = pos, proof_state = false}
+    ctxt ((Thm.theoremK, ""), [fact]);
 
 end;
 
@@ -393,7 +396,7 @@
 
 fun print_consts int pos ctxt pred cs =
   if null cs orelse no_print int ctxt then ()
-  else Output.state (Pretty.string_of (pretty_consts pos ctxt pred cs));
+  else Pretty.writeln (pretty_consts pos ctxt pred cs);
 
 end;
 

--- a/src/Pure/Isar/specification.ML	Wed Jul 26 15:42:13 2023 +0200
+++ b/src/Pure/Isar/specification.ML	Wed Jul 26 20:15:31 2023 +0200
@@ -343,7 +343,10 @@
       |> Attrib.partial_evaluation ctxt'
       |> Attrib.transform_facts (Proof_Context.export_morphism ctxt' lthy);
     val (res, lthy') = lthy |> Local_Theory.notes_kind kind facts';
-    val _ = Proof_Display.print_results int (Position.thread_data ()) lthy' ((kind, ""), res);
+    val _ =
+      Proof_Display.print_results
+        {interactive = int, pos = Position.thread_data (), proof_state = false}
+        lthy' ((kind, ""), res);
   in (res, lthy') end;
 
 in
@@ -396,6 +399,9 @@
     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};
+
     fun after_qed' results goal_ctxt' =
       let
         val results' =
@@ -406,13 +412,13 @@
             Local_Theory.notes_kind kind
               (map2 (fn (b, _) => fn ths => (b, [(ths, [])])) stmt results') lthy;
         val lthy'' =
-          if Binding.is_empty_atts (name, atts) then
-            (Proof_Display.print_results int pos lthy' ((kind, ""), res); lthy')
+          if Binding.is_empty_atts (name, atts)
+          then (print_results lthy' ((kind, ""), res); lthy')
           else
             let
               val ([(res_name, _)], lthy'') =
                 Local_Theory.notes_kind kind [((name, atts), [(maps #2 res, [])])] lthy';
-              val _ = Proof_Display.print_results int pos lthy' ((kind, res_name), res);
+              val _ = print_results lthy' ((kind, res_name), res);
             in lthy'' end;
       in after_qed results' lthy'' end;
 

--- a/src/Pure/Isar/toplevel.ML	Wed Jul 26 15:42:13 2023 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed Jul 26 20:15:31 2023 +0200
@@ -456,7 +456,7 @@
           val _ =
             (case Local_Theory.pretty lthy of
               [] => ()
-            | prts => Output.state (Pretty.string_of (Pretty.chunks prts)));
+            | prts => Pretty.writeln (Pretty.chunks prts));
         in (Theory gthy, lthy) end
     | _ => raise UNDEF));
 

--- a/src/Pure/ex/Guess.thy	Wed Jul 26 15:42:13 2023 +0200
+++ b/src/Pure/ex/Guess.thy	Wed Jul 26 20:15:31 2023 +0200
@@ -149,7 +149,8 @@
     val goal = Var guess;
     val pos = Position.thread_data ();
     fun print_result ctxt' (k, [(s, [_, th])]) =
-      Proof_Display.print_results int pos ctxt' (k, [(s, [th])]);
+      Proof_Display.print_results {interactive = int, pos = pos, proof_state = true}
+        ctxt' (k, [(s, [th])]);
     val before_qed =
       Method.primitive_text (fn ctxt =>
         Goal.conclude #> Raw_Simplifier.norm_hhf ctxt #>