# HG changeset patch
# User wenzelm
# Date 1667556700 -3600
# Node ID ae62064849f000e1a7af8ea2bd897efa93a70fc7
# Parent  e800cc580c80f8b0e14a650972b94dd3a81b8d92
tuned;

diff -r e800cc580c80 -r ae62064849f0 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Thu Nov 03 21:09:37 2022 +0100
+++ b/src/Pure/PIDE/command.ML	Fri Nov 04 11:11:40 2022 +0100
@@ -362,7 +362,7 @@
   make_print ("", [serial_string ()])
     {delay = NONE, pri = pri, persistent = true, strict = true, print_fn = print_fn};
 
-fun print command_visible command_overlays keywords command_name eval old_prints =
+fun print visible overlays keywords command_name eval old_prints =
   let
     val print_functions = Synchronized.value print_functions;
 
@@ -392,8 +392,8 @@
     val retained_prints =
       filter (fn print => print_finished print andalso print_persistent print) old_prints;
     val visible_prints =
-      if command_visible then
-        fold (fn (name, _) => cons (name, [])) print_functions command_overlays
+      if visible then
+        fold (fn (name, _) => cons (name, [])) print_functions overlays
         |> sort_distinct overlay_ord
         |> map_filter get_print
       else [];
diff -r e800cc580c80 -r ae62064849f0 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Thu Nov 03 21:09:37 2022 +0100
+++ b/src/Pure/PIDE/document.ML	Fri Nov 04 11:11:40 2022 +0100
@@ -147,10 +147,10 @@
     (header, keywords, make_perspective args, entries, result, consolidated));
 
 val required_node = #required o get_perspective;
-val visible_command = Inttab.defined o #visible o get_perspective;
+val command_overlays = Inttab.lookup_list o #overlays o get_perspective;
+val command_visible = Inttab.defined o #visible o get_perspective;
 val visible_last = #visible_last o get_perspective;
 val visible_node = is_some o visible_last
-val overlays = Inttab.lookup_list o #overlays o get_perspective;
 
 fun map_entries f =
   map_node (fn (header, keywords, perspective, entries, result, consolidated) =>
@@ -680,13 +680,11 @@
             (case opt_exec of
               SOME (eval, prints) =>
                 let
-                  val command_visible = visible_command node command_id;
-                  val command_overlays = overlays node command_id;
+                  val visible = command_visible node command_id;
+                  val overlays = command_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 of
+                  (case Command.print visible overlays keywords command_name eval prints of
                     SOME prints' => assign_update_new (command_id, SOME (eval, prints'))
                   | NONE => I)
                 end
@@ -708,8 +706,8 @@
   if not proper_init andalso is_none init then NONE
   else
     let
-      val command_visible = visible_command node command_id';
-      val command_overlays = overlays node command_id';
+      val visible = command_visible node command_id';
+      val overlays = command_overlays node command_id';
       val (command_name, blob_digests, blobs_index, span0) = the_command state command_id';
       val blobs = map (resolve_blob state) blob_digests;
       val span = Lazy.force span0;
@@ -717,8 +715,7 @@
       val eval' =
         Command.eval keywords (master_directory node) (fn () => the_default illegal_init init span)
           (blobs, blobs_index) command_id' span (#1 (#2 command_exec));
-      val prints' =
-        perhaps (Command.print command_visible command_overlays keywords command_name eval') [];
+      val prints' = perhaps (Command.print visible overlays keywords command_name eval') [];
       val exec' = (eval', prints');
 
       val assign_update' = assign_update_new (command_id', SOME exec') assign_update;