# HG changeset patch
# User wenzelm
# Date 1662542749 -7200
# Node ID 0f48e873e187d98d488d3dfd066948f36f62b3e7
# Parent  6508c21734f1ba305fae68de42f9f2e03f7e7a08
clarified message channel for 'print_state' (NB: the command was originally for TTY or Proof General);

diff -r 6508c21734f1 -r 0f48e873e187 NEWS
--- a/NEWS	Wed Sep 07 11:17:46 2022 +0200
+++ b/NEWS	Wed Sep 07 11:25:49 2022 +0200
@@ -37,6 +37,13 @@
 in building a session.
 
 
+*** Isabelle/jEdit Prover IDE ***
+
+* Command 'print_state' outputs a plain message ("writeln" instead of
+"state"). Thus it is displayed in the Output panel, even if the option
+"editor_output_state" is disabled.
+
+
 *** Isabelle/VSCode Prover IDE ***
 
 * VSCodium, an open-source distribution of VSCode without MS telemetry,
diff -r 6508c21734f1 -r 0f48e873e187 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Wed Sep 07 11:17:46 2022 +0200
+++ b/src/Pure/Pure.thy	Wed Sep 07 11:25:49 2022 +0200
@@ -1302,7 +1302,7 @@
   Outer_Syntax.command \<^command_keyword>\<open>print_state\<close>
     "print current proof state (if present)"
     (opt_modes >> (fn modes =>
-      Toplevel.keep (Print_Mode.with_modes modes (Output.state o Toplevel.string_of_state))));
+      Toplevel.keep (Print_Mode.with_modes modes (Output.writeln o Toplevel.string_of_state))));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>welcome\<close> "print welcome message"