produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
authorwenzelm
Tue Jul 09 23:49:19 2013 +0200 (2013-07-09 ago)
changeset 5256918dde2cf7aa7
parent 52568 92ae3f0ca060
child 52570 26d84a0b9209
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
src/Pure/PIDE/document.ML
     1.1 --- a/src/Pure/PIDE/document.ML	Tue Jul 09 18:11:31 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Tue Jul 09 23:49:19 2013 +0200
     1.3 @@ -84,7 +84,7 @@
     1.4  fun set_perspective ids =
     1.5    map_node (fn (header, _, entries, result) => (header, make_perspective ids, entries, result));
     1.6  
     1.7 -val visible_commands = #1 o get_perspective;
     1.8 +val visible_command = Inttab.defined o #1 o get_perspective;
     1.9  val visible_last = #2 o get_perspective;
    1.10  val visible_node = is_some o visible_last
    1.11  
    1.12 @@ -279,6 +279,8 @@
    1.13      NONE => err_undef "command" command_id
    1.14    | SOME command => command);
    1.15  
    1.16 +val the_command_name = #1 oo the_command;
    1.17 +
    1.18  end;
    1.19  
    1.20  
    1.21 @@ -396,17 +398,34 @@
    1.22    is_some (Thy_Info.lookup_theory name) orelse
    1.23    can get_header node andalso (not full orelse is_some (get_result node));
    1.24  
    1.25 -fun last_common state last_visible node0 node =
    1.26 +fun check_prints prints (prints': Command.print list) =
    1.27 +  if eq_list (op = o pairself #exec_id) (prints, prints') then NONE
    1.28 +  else SOME prints';
    1.29 +
    1.30 +fun update_prints command_visible command_name eval prints =
    1.31 +  if command_visible then
    1.32 +    let
    1.33 +      val new_prints = Command.print command_name eval;
    1.34 +      val prints' =
    1.35 +        new_prints |> map (fn new_print =>
    1.36 +          (case find_first (fn {name, ...} => name = #name new_print) prints of
    1.37 +            SOME print => if Command.stable_print print then print else new_print
    1.38 +          | NONE => new_print));
    1.39 +    in check_prints prints prints' end
    1.40 +  else check_prints prints (filter Command.stable_print prints);
    1.41 +
    1.42 +fun last_common state node0 node =
    1.43    let
    1.44      fun update_flags prev (visible, initial) =
    1.45        let
    1.46 -        val visible' = visible andalso prev <> last_visible;
    1.47 +        val visible' = visible andalso prev <> visible_last node;
    1.48          val initial' = initial andalso
    1.49            (case prev of
    1.50              NONE => true
    1.51 -          | SOME id => not (Keyword.is_theory_begin (#1 (the_command state id))));
    1.52 +          | SOME command_id => not (Keyword.is_theory_begin (the_command_name state command_id)));
    1.53        in (visible', initial') end;
    1.54 -    fun get_common ((prev, id), opt_exec) (same, (_, flags)) =
    1.55 +
    1.56 +    fun get_common ((prev, command_id), opt_exec) (_, same, flags, assign_update) =
    1.57        if same then
    1.58          let
    1.59            val flags' = update_flags prev flags;
    1.60 @@ -414,20 +433,32 @@
    1.61              (case opt_exec of
    1.62                NONE => false
    1.63              | SOME (eval, _) =>
    1.64 -                (case lookup_entry node0 id of
    1.65 +                (case lookup_entry node0 command_id of
    1.66                    NONE => false
    1.67                  | SOME (eval0, _) =>
    1.68                      #exec_id eval = #exec_id eval0 andalso Command.stable_eval eval));
    1.69 -        in SOME (same', (prev, flags')) end
    1.70 +          val assign_update' = assign_update |>
    1.71 +            (case opt_exec of
    1.72 +              SOME (eval, prints) =>
    1.73 +                let
    1.74 +                  val command_visible = visible_command node command_id;
    1.75 +                  val command_name = the_command_name state command_id;
    1.76 +                in
    1.77 +                  (case update_prints command_visible command_name eval prints of
    1.78 +                    SOME prints' => assign_update_new (command_id, SOME (eval, prints'))
    1.79 +                  | NONE => I)
    1.80 +                end
    1.81 +            | NONE => I);
    1.82 +        in SOME (prev, same', flags', assign_update') end
    1.83        else NONE;
    1.84 -    val (same, (common, flags)) =
    1.85 -      iterate_entries get_common node (true, (NONE, (true, true)));
    1.86 -  in
    1.87 -    if same then
    1.88 -      let val last = Entries.get_after (get_entries node) common
    1.89 -      in (last, update_flags last flags) end
    1.90 -    else (common, flags)
    1.91 -  end;
    1.92 +    val (common, same, flags, assign_update') =
    1.93 +      iterate_entries get_common node (NONE, true, (true, true), assign_update_empty);
    1.94 +    val (common', flags') =
    1.95 +      if same then
    1.96 +        let val last = Entries.get_after (get_entries node) common
    1.97 +        in (last, update_flags last flags) end
    1.98 +      else (common, flags);
    1.99 +  in (assign_update', common', flags') end;
   1.100  
   1.101  fun illegal_init _ = error "Illegal theory header after end of theory";
   1.102  
   1.103 @@ -439,30 +470,13 @@
   1.104        val (command_name, span) = the_command state command_id' ||> Lazy.force;
   1.105  
   1.106        val eval' = Command.eval (fn () => the_default illegal_init init span) span eval;
   1.107 -      val prints' = if command_visible then Command.print command_name eval' else [];
   1.108 +      val prints' = perhaps (update_prints command_visible command_name eval') [];
   1.109        val exec' = (eval', prints');
   1.110  
   1.111        val assign_update' = assign_update_new (command_id', SOME exec') assign_update;
   1.112        val init' = if Keyword.is_theory_begin command_name then NONE else init;
   1.113      in SOME (assign_update', (command_id', (eval', prints')), init') end;
   1.114  
   1.115 -fun update_prints state node command_id assign_update =
   1.116 -  (case the_entry node command_id of
   1.117 -    SOME (eval, prints) =>
   1.118 -      let
   1.119 -        val (command_name, _) = the_command state command_id;
   1.120 -        val new_prints = Command.print command_name eval;
   1.121 -        val prints' =
   1.122 -          new_prints |> map (fn new_print =>
   1.123 -            (case find_first (fn {name, ...} => name = #name new_print) prints of
   1.124 -              SOME print => if Command.stable_print print then print else new_print
   1.125 -            | NONE => new_print));
   1.126 -      in
   1.127 -        if eq_list (op = o pairself #exec_id) (prints, prints') then assign_update
   1.128 -        else assign_update_new (command_id, SOME (eval, prints')) assign_update
   1.129 -      end
   1.130 -  | NONE => assign_update);
   1.131 -
   1.132  in
   1.133  
   1.134  fun update old_version_id new_version_id edits state =
   1.135 @@ -496,28 +510,18 @@
   1.136                        check_theory false name node andalso
   1.137                        forall (fn (name, (_, node)) => check_theory true name node) imports;
   1.138  
   1.139 -                    val visible_commands = visible_commands node;
   1.140 -                    val visible_command = Inttab.defined visible_commands;
   1.141 -                    val last_visible = visible_last node;
   1.142 -
   1.143 -                    val (common, (still_visible, initial)) =
   1.144 -                      if imports_changed then (NONE, (true, true))
   1.145 -                      else last_common state last_visible node0 node;
   1.146 -
   1.147 +                    val (print_execs, common, (still_visible, initial)) =
   1.148 +                      if imports_changed then (assign_update_empty, NONE, (true, true))
   1.149 +                      else last_common state node0 node;
   1.150                      val common_command_exec = the_default_entry node common;
   1.151  
   1.152 -                    val (new_execs, (command_id', (eval', _)), _) =
   1.153 -                      (assign_update_empty, common_command_exec, if initial then SOME init else NONE)
   1.154 +                    val (updated_execs, (command_id', (eval', _)), _) =
   1.155 +                      (print_execs, common_command_exec, if initial then SOME init else NONE)
   1.156                        |> (still_visible orelse node_required) ?
   1.157                          iterate_entries_after common
   1.158                            (fn ((prev, id), _) => fn res =>
   1.159 -                            if not node_required andalso prev = last_visible then NONE
   1.160 -                            else new_exec state proper_init (visible_command id) id res) node;
   1.161 -
   1.162 -                    val updated_execs =
   1.163 -                      (visible_commands, new_execs) |-> Inttab.fold (fn (command_id, ()) =>
   1.164 -                        not (assign_update_defined new_execs command_id) ?
   1.165 -                          update_prints state node command_id);
   1.166 +                            if not node_required andalso prev = visible_last node then NONE
   1.167 +                            else new_exec state proper_init (visible_command node id) id res) node;
   1.168  
   1.169                      val assigned_execs =
   1.170                        (node0, updated_execs) |-> iterate_entries_after common