src/Pure/PIDE/document.ML
changeset 52527 dbac84eab3bc
parent 52526 d234cb6b60e3
child 52530 99dd8b4ef3fe
     1.1 --- a/src/Pure/PIDE/document.ML	Thu Jul 04 16:04:53 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Thu Jul 04 23:51:47 2013 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4    val start_execution: state -> unit
     1.5    val timing: bool Unsynchronized.ref
     1.6    val update: version_id -> version_id -> edit list -> state ->
     1.7 -    (command_id * exec_id option) list * state
     1.8 +    (command_id * exec_id list) list * state
     1.9    val state: unit -> state
    1.10    val change_state: (state -> state) -> unit
    1.11  end;
    1.12 @@ -61,11 +61,13 @@
    1.13  type exec = exec_id * (Command.eval * Command.print list);  (*eval/print process*)
    1.14  val no_exec: exec = (no_id, (Command.no_eval, []));
    1.15  
    1.16 +fun exec_ids_of ((exec_id, (_, prints)): exec) = exec_id :: map #exec_id prints;
    1.17 +
    1.18  fun exec_result ((_, (eval, _)): exec) = Command.memo_result eval;
    1.19  
    1.20  fun exec_run ((_, (eval, prints)): exec) =
    1.21   (Command.memo_eval eval;
    1.22 -  prints |> List.app (fn {name, pri, print} =>
    1.23 +  prints |> List.app (fn {name, pri, print, ...} =>
    1.24      Command.memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true} print));
    1.25  
    1.26  
    1.27 @@ -121,7 +123,6 @@
    1.28    map_node (fn (header, _, entries, result) => (header, make_perspective ids, entries, result));
    1.29  
    1.30  val visible_commands = #1 o get_perspective;
    1.31 -val visible_command = Inttab.defined o visible_commands;
    1.32  val visible_last = #2 o get_perspective;
    1.33  val visible_node = is_some o visible_last
    1.34  
    1.35 @@ -313,10 +314,14 @@
    1.36  
    1.37  (* consolidated states *)
    1.38  
    1.39 -fun stable_command ((exec_id, (eval, prints)): exec) =
    1.40 -  not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id))) andalso
    1.41 -  Command.memo_stable eval andalso
    1.42 -  forall (Command.memo_stable o #print) prints;
    1.43 +fun stable_goals exec_id =
    1.44 +  not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id)));
    1.45 +
    1.46 +fun stable_eval ((exec_id, (eval, _)): exec) =
    1.47 +  stable_goals exec_id andalso Command.memo_stable eval;
    1.48 +
    1.49 +fun stable_print ({exec_id, print, ...}: Command.print) =
    1.50 +  stable_goals exec_id andalso Command.memo_stable print;
    1.51  
    1.52  fun finished_theory node =
    1.53    (case Exn.capture (Command.memo_result o the) (get_result node) of
    1.54 @@ -422,7 +427,7 @@
    1.55              | SOME (exec_id, exec) =>
    1.56                  (case lookup_entry node0 id of
    1.57                    NONE => false
    1.58 -                | SOME (exec_id0, _) => exec_id = exec_id0 andalso stable_command (exec_id, exec)));
    1.59 +                | SOME (exec_id0, _) => exec_id = exec_id0 andalso stable_eval (exec_id, exec)));
    1.60          in SOME (same', (prev, flags')) end
    1.61        else NONE;
    1.62      val (same, (common, flags)) =
    1.63 @@ -438,11 +443,11 @@
    1.64    if not proper_init andalso is_none init then NONE
    1.65    else
    1.66      let
    1.67 -      val (name, span) = the_command state command_id' ||> Lazy.force;
    1.68 +      val (command_name, span) = the_command state command_id' ||> Lazy.force;
    1.69  
    1.70        fun illegal_init _ = error "Illegal theory header after end of theory";
    1.71        val (modify_init, init') =
    1.72 -        if Keyword.is_theory_begin name then
    1.73 +        if Keyword.is_theory_begin command_name then
    1.74            (Toplevel.modify_init (fn () => the_default illegal_init init span), NONE)
    1.75          else (I, init);
    1.76  
    1.77 @@ -456,13 +461,29 @@
    1.78                  (fn () =>
    1.79                    Command.read span
    1.80                    |> modify_init
    1.81 -                  |> Toplevel.put_id (print_id exec_id')) ();
    1.82 +                  |> Toplevel.put_id exec_id') ();
    1.83            in Command.eval span tr eval_state end);
    1.84 -      val prints' = if command_visible then Command.print name eval' else [];
    1.85 -
    1.86 +      val prints' = if command_visible then Command.print new_id command_name eval' else [];
    1.87        val command_exec' = (command_id', (exec_id', (eval', prints')));
    1.88      in SOME (command_exec' :: execs, command_exec', init') end;
    1.89  
    1.90 +fun update_prints state node command_id =
    1.91 +  (case the_entry node command_id of
    1.92 +    SOME (exec_id, (eval, prints)) =>
    1.93 +      let
    1.94 +        val (command_name, _) = the_command state command_id;
    1.95 +        val new_prints = Command.print new_id command_name eval;
    1.96 +        val prints' =
    1.97 +          new_prints |> map (fn new_print =>
    1.98 +            (case find_first (fn {name, ...} => name = #name new_print) prints of
    1.99 +              SOME print => if stable_print print then print else new_print
   1.100 +            | NONE => new_print));
   1.101 +      in
   1.102 +        if eq_list (op = o pairself #exec_id) (prints, prints') then NONE
   1.103 +        else SOME (command_id, (exec_id, (eval, prints')))
   1.104 +      end
   1.105 +  | NONE => NONE);
   1.106 +
   1.107  in
   1.108  
   1.109  fun update (old_id: version_id) (new_id: version_id) edits state =
   1.110 @@ -483,10 +504,10 @@
   1.111              (fn () =>
   1.112                let
   1.113                  val imports = map (apsnd Future.join) deps;
   1.114 -                val updated_imports = exists (is_some o #3 o #1 o #2) imports;
   1.115 +                val changed_imports = exists (#4 o #1 o #2) imports;
   1.116                  val node_required = is_required name;
   1.117                in
   1.118 -                if updated_imports orelse AList.defined (op =) edits name orelse
   1.119 +                if changed_imports orelse AList.defined (op =) edits name orelse
   1.120                    not (stable_entries node) orelse not (finished_theory node)
   1.121                  then
   1.122                    let
   1.123 @@ -496,9 +517,12 @@
   1.124                        check_theory false name node andalso
   1.125                        forall (fn (name, (_, node)) => check_theory true name node) imports;
   1.126  
   1.127 +                    val visible_commands = visible_commands node;
   1.128 +                    val visible_command = Inttab.defined visible_commands;
   1.129                      val last_visible = visible_last node;
   1.130 +
   1.131                      val (common, (still_visible, initial)) =
   1.132 -                      if updated_imports then (NONE, (true, true))
   1.133 +                      if changed_imports then (NONE, (true, true))
   1.134                        else last_common state last_visible node0 node;
   1.135                      val common_command_exec = the_default_entry node common;
   1.136  
   1.137 @@ -508,13 +532,18 @@
   1.138                          iterate_entries_after common
   1.139                            (fn ((prev, id), _) => fn res =>
   1.140                              if not node_required andalso prev = last_visible then NONE
   1.141 -                            else new_exec state proper_init (visible_command node id) id res) node;
   1.142 +                            else new_exec state proper_init (visible_command id) id res) node;
   1.143 +
   1.144 +                    val updated_execs =
   1.145 +                      (visible_commands, new_execs) |-> Inttab.fold (fn (id, ()) =>
   1.146 +                        if exists (fn (_, (id', _)) => id = id') new_execs then I
   1.147 +                        else append (the_list (update_prints state node id)));
   1.148  
   1.149                      val no_execs =
   1.150                        iterate_entries_after common
   1.151                          (fn ((_, id0), exec0) => fn res =>
   1.152                            if is_none exec0 then NONE
   1.153 -                          else if exists (fn (_, (id, _)) => id0 = id) new_execs
   1.154 +                          else if exists (fn (_, (id, _)) => id0 = id) updated_execs
   1.155                            then SOME res
   1.156                            else SOME (id0 :: res)) node0 [];
   1.157  
   1.158 @@ -525,20 +554,21 @@
   1.159  
   1.160                      val node' = node
   1.161                        |> fold reset_entry no_execs
   1.162 -                      |> fold (fn (id, exec) => update_entry id (SOME exec)) new_execs
   1.163 -                      |> entries_stable (null new_execs)
   1.164 +                      |> fold (fn (id, exec) => update_entry id (SOME exec)) updated_execs
   1.165 +                      |> entries_stable (null updated_execs)
   1.166                        |> set_result result;
   1.167                      val updated_node =
   1.168 -                      if null no_execs andalso null new_execs then NONE
   1.169 +                      if null no_execs andalso null updated_execs then NONE
   1.170                        else SOME (name, node');
   1.171 -                  in ((no_execs, new_execs, updated_node), node') end
   1.172 -                else (([], [], NONE), node)
   1.173 +                    val changed_result = not (null no_execs) orelse not (null new_execs);
   1.174 +                  in ((no_execs, updated_execs, updated_node, changed_result), node') end
   1.175 +                else (([], [], NONE, false), node)
   1.176                end))
   1.177        |> Future.joins |> map #1);
   1.178  
   1.179      val command_execs =
   1.180 -      map (rpair NONE) (maps #1 updated) @
   1.181 -      map (fn (command_id, (exec_id, _)) => (command_id, SOME exec_id)) (maps #2 updated);
   1.182 +      map (rpair []) (maps #1 updated) @
   1.183 +      map (fn (command_id, exec) => (command_id, exec_ids_of exec)) (maps #2 updated);
   1.184      val updated_nodes = map_filter #3 updated;
   1.185  
   1.186      val state' = state