src/Pure/PIDE/document.ML
changeset 52566 52a0eacf04d1
parent 52536 3a35ce87a55c
child 52569 18dde2cf7aa7
     1.1 --- a/src/Pure/PIDE/document.ML	Tue Jul 09 16:32:51 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Tue Jul 09 17:58:38 2013 +0200
     1.3 @@ -108,6 +108,12 @@
     1.4  fun set_result result =
     1.5    map_node (fn (header, perspective, entries, _) => (header, perspective, entries, result));
     1.6  
     1.7 +fun changed_result node node' =
     1.8 +  (case (get_result node, get_result node') of
     1.9 +    (SOME eval, SOME eval') => #exec_id eval <> #exec_id eval'
    1.10 +  | (NONE, NONE) => false
    1.11 +  | _ => true);
    1.12 +
    1.13  fun finished_theory node =
    1.14    (case Exn.capture (Command.eval_result_state o the) (get_result node) of
    1.15      Exn.Res st => can (Toplevel.end_theory Position.none) st
    1.16 @@ -144,11 +150,9 @@
    1.17  fun the_default_entry node (SOME id) = (id, the_default Command.no_exec (the_entry node id))
    1.18    | the_default_entry _ NONE = (Document_ID.none, Command.no_exec);
    1.19  
    1.20 -fun update_entry id exec =
    1.21 -  map_entries (Entries.update (id, exec));
    1.22 -
    1.23 -fun reset_entry id node =
    1.24 -  if is_some (lookup_entry node id) then update_entry id NONE node else node;
    1.25 +fun assign_entry (command_id, exec) node =
    1.26 +  if is_none (Entries.lookup (get_entries node) command_id) then node
    1.27 +  else map_entries (Entries.update (command_id, exec)) node;
    1.28  
    1.29  fun reset_after id entries =
    1.30    (case Entries.get_after entries id of
    1.31 @@ -277,6 +281,9 @@
    1.32  
    1.33  end;
    1.34  
    1.35 +
    1.36 +(* remove_versions *)
    1.37 +
    1.38  fun remove_versions version_ids state = state |> map_state (fn (versions, _, execution) =>
    1.39    let
    1.40      val _ =
    1.41 @@ -327,6 +334,25 @@
    1.42  
    1.43  (** document update **)
    1.44  
    1.45 +(* exec state assignment *)
    1.46 +
    1.47 +type assign_update = Command.exec option Inttab.table;  (*command id -> exec*)
    1.48 +
    1.49 +val assign_update_empty: assign_update = Inttab.empty;
    1.50 +fun assign_update_null (tab: assign_update) = Inttab.is_empty tab;
    1.51 +fun assign_update_defined (tab: assign_update) command_id = Inttab.defined tab command_id;
    1.52 +fun assign_update_apply (tab: assign_update) node = Inttab.fold assign_entry tab node;
    1.53 +
    1.54 +fun assign_update_new upd (tab: assign_update) =
    1.55 +  Inttab.update_new upd tab
    1.56 +    handle Inttab.DUP dup => err_dup "exec state assignment" dup;
    1.57 +
    1.58 +fun assign_update_result (tab: assign_update) =
    1.59 +  Inttab.fold (fn (command_id, exec) => cons (command_id, Command.exec_ids exec)) tab [];
    1.60 +
    1.61 +
    1.62 +(* update *)
    1.63 +
    1.64  val timing = Unsynchronized.ref false;
    1.65  fun timeit msg e = cond_timeit (! timing) msg e;
    1.66  
    1.67 @@ -405,19 +431,22 @@
    1.68  
    1.69  fun illegal_init _ = error "Illegal theory header after end of theory";
    1.70  
    1.71 -fun new_exec state proper_init command_visible command_id' (execs, command_exec, init) =
    1.72 +fun new_exec state proper_init command_visible command_id' (assign_update, command_exec, init) =
    1.73    if not proper_init andalso is_none init then NONE
    1.74    else
    1.75      let
    1.76        val (_, (eval, _)) = command_exec;
    1.77        val (command_name, span) = the_command state command_id' ||> Lazy.force;
    1.78 -      val init' = if Keyword.is_theory_begin command_name then NONE else init;
    1.79 +
    1.80        val eval' = Command.eval (fn () => the_default illegal_init init span) span eval;
    1.81        val prints' = if command_visible then Command.print command_name eval' else [];
    1.82 -      val command_exec' = (command_id', (eval', prints'));
    1.83 -    in SOME (command_exec' :: execs, command_exec', init') end;
    1.84 +      val exec' = (eval', prints');
    1.85  
    1.86 -fun update_prints state node command_id =
    1.87 +      val assign_update' = assign_update_new (command_id', SOME exec') assign_update;
    1.88 +      val init' = if Keyword.is_theory_begin command_name then NONE else init;
    1.89 +    in SOME (assign_update', (command_id', (eval', prints')), init') end;
    1.90 +
    1.91 +fun update_prints state node command_id assign_update =
    1.92    (case the_entry node command_id of
    1.93      SOME (eval, prints) =>
    1.94        let
    1.95 @@ -429,10 +458,10 @@
    1.96                SOME print => if Command.stable_print print then print else new_print
    1.97              | NONE => new_print));
    1.98        in
    1.99 -        if eq_list (op = o pairself #exec_id) (prints, prints') then NONE
   1.100 -        else SOME (command_id, (eval, prints'))
   1.101 +        if eq_list (op = o pairself #exec_id) (prints, prints') then assign_update
   1.102 +        else assign_update_new (command_id, SOME (eval, prints')) assign_update
   1.103        end
   1.104 -  | NONE => NONE);
   1.105 +  | NONE => assign_update);
   1.106  
   1.107  in
   1.108  
   1.109 @@ -454,10 +483,10 @@
   1.110              (fn () =>
   1.111                let
   1.112                  val imports = map (apsnd Future.join) deps;
   1.113 -                val changed_imports = exists (#4 o #1 o #2) imports;
   1.114 +                val imports_changed = exists (#3 o #1 o #2) imports;
   1.115                  val node_required = is_required name;
   1.116                in
   1.117 -                if changed_imports orelse AList.defined (op =) edits name orelse
   1.118 +                if imports_changed orelse AList.defined (op =) edits name orelse
   1.119                    not (stable_entries node) orelse not (finished_theory node)
   1.120                  then
   1.121                    let
   1.122 @@ -472,59 +501,54 @@
   1.123                      val last_visible = visible_last node;
   1.124  
   1.125                      val (common, (still_visible, initial)) =
   1.126 -                      if changed_imports then (NONE, (true, true))
   1.127 +                      if imports_changed then (NONE, (true, true))
   1.128                        else last_common state last_visible node0 node;
   1.129 +
   1.130                      val common_command_exec = the_default_entry node common;
   1.131  
   1.132                      val (new_execs, (command_id', (eval', _)), _) =
   1.133 -                      ([], common_command_exec, if initial then SOME init else NONE) |>
   1.134 -                      (still_visible orelse node_required) ?
   1.135 +                      (assign_update_empty, common_command_exec, if initial then SOME init else NONE)
   1.136 +                      |> (still_visible orelse node_required) ?
   1.137                          iterate_entries_after common
   1.138                            (fn ((prev, id), _) => fn res =>
   1.139                              if not node_required andalso prev = last_visible then NONE
   1.140                              else new_exec state proper_init (visible_command id) id res) node;
   1.141  
   1.142                      val updated_execs =
   1.143 -                      (visible_commands, new_execs) |-> Inttab.fold (fn (id, ()) =>
   1.144 -                        if exists (fn (_, ({exec_id = id', ...}, _)) => id = id') new_execs then I
   1.145 -                        else append (the_list (update_prints state node id)));
   1.146 +                      (visible_commands, new_execs) |-> Inttab.fold (fn (command_id, ()) =>
   1.147 +                        not (assign_update_defined new_execs command_id) ?
   1.148 +                          update_prints state node command_id);
   1.149  
   1.150 -                    val no_execs =
   1.151 -                      iterate_entries_after common
   1.152 -                        (fn ((_, id0), exec0) => fn res =>
   1.153 +                    val assigned_execs =
   1.154 +                      (node0, updated_execs) |-> iterate_entries_after common
   1.155 +                        (fn ((_, command_id0), exec0) => fn res =>
   1.156                            if is_none exec0 then NONE
   1.157 -                          else if exists (fn (_, ({exec_id = id, ...}, _)) => id0 = id) updated_execs
   1.158 -                          then SOME res
   1.159 -                          else SOME (id0 :: res)) node0 [];
   1.160 +                          else if assign_update_defined updated_execs command_id0 then SOME res
   1.161 +                          else SOME (assign_update_new (command_id0, NONE) res));
   1.162  
   1.163                      val last_exec =
   1.164                        if command_id' = Document_ID.none then NONE else SOME command_id';
   1.165                      val result =
   1.166 -                      if is_some (after_entry node last_exec) then NONE
   1.167 +                      if is_none last_exec orelse is_some (after_entry node last_exec) then NONE
   1.168                        else SOME eval';
   1.169  
   1.170                      val node' = node
   1.171 -                      |> fold reset_entry no_execs
   1.172 -                      |> fold (fn (id, exec) => update_entry id (SOME exec)) updated_execs
   1.173 -                      |> entries_stable (null updated_execs)
   1.174 +                      |> assign_update_apply assigned_execs
   1.175 +                      |> entries_stable (assign_update_null updated_execs)
   1.176                        |> set_result result;
   1.177 -                    val updated_node =
   1.178 -                      if null no_execs andalso null updated_execs then NONE
   1.179 -                      else SOME (name, node');
   1.180 -                    val changed_result = not (null no_execs) orelse not (null new_execs);
   1.181 -                  in ((no_execs, updated_execs, updated_node, changed_result), node') end
   1.182 -                else (([], [], NONE, false), node)
   1.183 +                    val assigned_node =
   1.184 +                      if assign_update_null assigned_execs then NONE else SOME (name, node');
   1.185 +                    val result_changed = changed_result node0 node';
   1.186 +                  in
   1.187 +                    ((assign_update_result assigned_execs, assigned_node, result_changed), node')
   1.188 +                  end
   1.189 +                else (([], NONE, false), node)
   1.190                end))
   1.191        |> Future.joins |> map #1);
   1.192  
   1.193 -    val command_execs =
   1.194 -      map (rpair []) (maps #1 updated) @
   1.195 -      map (fn (command_id, exec) => (command_id, Command.exec_ids exec)) (maps #2 updated);
   1.196 -    val updated_nodes = map_filter #3 updated;
   1.197 -
   1.198      val state' = state
   1.199 -      |> define_version new_version_id (fold put_node updated_nodes new_version);
   1.200 -  in (command_execs, state') end;
   1.201 +      |> define_version new_version_id (fold put_node (map_filter #2 updated) new_version);
   1.202 +  in (maps #1 updated, state') end;
   1.203  
   1.204  end;
   1.205