src/Pure/PIDE/document.ML

 
 val required_node = #required o get_perspective;
 val visible_command = 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 = #overlays o get_perspective;
+val overlays = Inttab.lookup_list o #overlays o get_perspective;
 
 fun map_entries f =
   map_node (fn (header, perspective, entries, result) => (header, perspective, f entries, result));
 fun get_entries (Node {entries, ...}) = entries;
 

           val assign_update' = assign_update |> ok' ?
             (case opt_exec of
               SOME (eval, prints) =>
                 let
                   val command_visible = visible_command node command_id;
+                  val command_overlays = overlays node command_id;
                   val command_name = the_command_name state command_id;
                 in
-                  (case Command.print command_visible command_name eval prints of
+                  (case Command.print command_visible command_overlays command_name eval prints of
                     SOME prints' => assign_update_new (command_id, SOME (eval, prints'))
                   | NONE => I)
                 end
             | NONE => I);
         in SOME (prev, ok', flags', assign_update') end

       else (common, flags);
   in (assign_update', common', flags') end;
 
 fun illegal_init _ = error "Illegal theory header after end of theory";
 
-fun new_exec state proper_init command_visible command_id' (assign_update, command_exec, init) =
+fun new_exec state node proper_init command_id' (assign_update, command_exec, init) =
   if not proper_init andalso is_none init then NONE
   else
     let
       val (_, (eval, _)) = command_exec;
+
+      val command_visible = visible_command node command_id';
+      val command_overlays = overlays node command_id';
       val (command_name, span) = the_command state command_id' ||> Lazy.force;
 
       val eval' = Command.eval (fn () => the_default illegal_init init span) span eval;
-      val prints' = perhaps (Command.print command_visible command_name eval') [];
+      val prints' = perhaps (Command.print command_visible command_overlays command_name eval') [];
       val exec' = (eval', prints');
 
       val assign_update' = assign_update_new (command_id', SOME exec') assign_update;
       val init' = if Keyword.is_theory_begin command_name then NONE else init;
     in SOME (assign_update', (command_id', (eval', prints')), init') end;

                       (print_execs, common_command_exec, if initial then SOME init else NONE)
                       |> (still_visible orelse node_required) ?
                         iterate_entries_after common
                           (fn ((prev, id), _) => fn res =>
                             if not node_required andalso prev = visible_last node then NONE
-                            else new_exec state proper_init (visible_command node id) id res) node;
+                            else new_exec state node proper_init id res) node;
 
                     val assigned_execs =
                       (node0, updated_execs) |-> iterate_entries_after common
                         (fn ((_, command_id0), exec0) => fn res =>
                           if is_none exec0 then NONE