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