src/Pure/PIDE/document.ML
changeset 52850 9fff9f78240a
parent 52849 199e9fa5a5c2
child 52862 930ce8eacb87
     1.1 --- a/src/Pure/PIDE/document.ML	Fri Aug 02 14:26:09 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Fri Aug 02 16:00:14 2013 +0200
     1.3 @@ -100,7 +100,7 @@
     1.4  val visible_command = Inttab.defined o #visible o get_perspective;
     1.5  val visible_last = #visible_last o get_perspective;
     1.6  val visible_node = is_some o visible_last
     1.7 -val overlays = #overlays o get_perspective;
     1.8 +val overlays = Inttab.lookup_list o #overlays o get_perspective;
     1.9  
    1.10  fun map_entries f =
    1.11    map_node (fn (header, perspective, entries, result) => (header, perspective, f entries, result));
    1.12 @@ -442,9 +442,10 @@
    1.13                SOME (eval, prints) =>
    1.14                  let
    1.15                    val command_visible = visible_command node command_id;
    1.16 +                  val command_overlays = overlays node command_id;
    1.17                    val command_name = the_command_name state command_id;
    1.18                  in
    1.19 -                  (case Command.print command_visible command_name eval prints of
    1.20 +                  (case Command.print command_visible command_overlays command_name eval prints of
    1.21                      SOME prints' => assign_update_new (command_id, SOME (eval, prints'))
    1.22                    | NONE => I)
    1.23                  end
    1.24 @@ -462,15 +463,18 @@
    1.25  
    1.26  fun illegal_init _ = error "Illegal theory header after end of theory";
    1.27  
    1.28 -fun new_exec state proper_init command_visible command_id' (assign_update, command_exec, init) =
    1.29 +fun new_exec state node proper_init command_id' (assign_update, command_exec, init) =
    1.30    if not proper_init andalso is_none init then NONE
    1.31    else
    1.32      let
    1.33        val (_, (eval, _)) = command_exec;
    1.34 +
    1.35 +      val command_visible = visible_command node command_id';
    1.36 +      val command_overlays = overlays node command_id';
    1.37        val (command_name, span) = the_command state command_id' ||> Lazy.force;
    1.38  
    1.39        val eval' = Command.eval (fn () => the_default illegal_init init span) span eval;
    1.40 -      val prints' = perhaps (Command.print command_visible command_name eval') [];
    1.41 +      val prints' = perhaps (Command.print command_visible command_overlays command_name eval') [];
    1.42        val exec' = (eval', prints');
    1.43  
    1.44        val assign_update' = assign_update_new (command_id', SOME exec') assign_update;
    1.45 @@ -525,7 +529,7 @@
    1.46                          iterate_entries_after common
    1.47                            (fn ((prev, id), _) => fn res =>
    1.48                              if not node_required andalso prev = visible_last node then NONE
    1.49 -                            else new_exec state proper_init (visible_command node id) id res) node;
    1.50 +                            else new_exec state node proper_init id res) node;
    1.51  
    1.52                      val assigned_execs =
    1.53                        (node0, updated_execs) |-> iterate_entries_after common