tuned;
authorwenzelm
Thu, 03 Nov 2022 20:42:27 +0100
changeset 76417 e937d14b58e2
parent 76416 22746dfa75a1
child 76418 2b0ff7c52aa4
tuned;
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