# HG changeset patch
# User wenzelm
# Date 1667504547 -3600
# Node ID e937d14b58e287a3257fb11a20290afbd34dafde
# Parent  22746dfa75a18b95df6f108314a4a57d1dd65f3f
tuned;

diff -r 22746dfa75a1 -r e937d14b58e2 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Thu Nov 03 20:33:59 2022 +0100
+++ b/src/Pure/PIDE/document.ML	Thu Nov 03 20:42:27 2022 +0100
@@ -683,10 +683,10 @@
                   val command_visible = visible_command node command_id;
                   val command_overlays = overlays node command_id;
                   val command_name = the_command_name state command_id;
+                  val command_print =
+                    Command.print command_visible command_overlays keywords command_name eval prints;
                 in
-                  (case
-                    Command.print command_visible command_overlays keywords command_name eval prints
-                   of
+                  (case command_print of
                     SOME prints' => assign_update_new (command_id, SOME (eval, prints'))
                   | NONE => I)
                 end