# HG changeset patch
# User wenzelm
# Date 1314366990 -7200
# Node ID 38c5b085fb1cd71c49c1a859966b9302b561802b
# Parent  9a04e7502e22e56211452d0cf2e0449f6161f1e4
improved Document.edit: more accurate update_start and no_execs;
tuned;

diff -r 9a04e7502e22 -r 38c5b085fb1c src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Fri Aug 26 15:09:54 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Fri Aug 26 15:56:30 2011 +0200
@@ -145,6 +145,11 @@
     NONE => err_undef "command entry" id
   | SOME (_, next) => next);
 
+fun lookup_entry (Node {entries, ...}) id =
+  (case Entries.lookup entries id of
+    NONE => NONE
+  | SOME (exec, _) => exec);
+
 fun the_entry (Node {entries, ...}) id =
   (case Entries.lookup entries id of
     NONE => err_undef "command entry" id
@@ -376,14 +381,6 @@
 
 local
 
-fun after_perspective node ((prev, _), _) = #2 (get_perspective node) = prev;
-
-fun needs_update node0 ((_, id), SOME exec) =
-      (case try (the_entry node0) id of
-        SOME (SOME exec0) => exec0 <> exec
-      | _ => true)
-  | needs_update _ _ = true;
-
 fun init_theory deps name node =
   let
     val (thy_name, imports, uses) = Exn.release (get_header node);
@@ -401,6 +398,9 @@
               (#2 (Future.join (the (AList.lookup (op =) deps import))))));
   in Thy_Load.begin_theory dir thy_name imports files parents end;
 
+fun after_perspective node ((prev, _), _) = prev = #2 (get_perspective node);
+fun needs_update node0 ((_, id), exec) = is_none exec orelse exec <> lookup_entry node0 id;
+
 fun new_exec state init command_id' (execs, exec) =
   let
     val command' = the_command state command_id';
@@ -434,27 +434,22 @@
             in
               (case first_entry NONE (after_perspective node orf needs_update node0) node of
                 NONE => Future.value (([], [], []), set_touched false node)
-              | SOME ((prev, id), _) =>
+              | SOME (entry as ((prev, id), _)) =>
                   (singleton o Future.forks)
                     {name = "Document.edit", group = NONE,
                       deps = map (Future.task_of o #2) deps, pri = 0, interrupts = false}
                     (fn () =>
                       let
-                        val (execs, exec) =
-                          fold_entries (SOME id)
-                            (fn entry1 as ((_, id1), _) => fn res =>
-                              if after_perspective node entry1 then NONE
-                              else SOME (new_exec state init id1 res))
-                            node ([], the_exec state (the_default_entry node prev));
+                        val update_start =
+                          Option.map (#2 o #1) (first_entry (SOME id) (needs_update node0) node);
 
-                        val no_execs =
-                          if can (the_entry node0) id then
-                            fold_entries (SOME id)
-                              (fn ((_, id0), exec0) => fn res =>
-                                if is_none exec0 then NONE
-                                else if exists (fn (_, (id1, _)) => id0 = id1) execs then SOME res
-                                else SOME (id0 :: res)) node0 []
-                          else [];
+                        val (execs, exec) =
+                          ([], the_exec state (the_default_entry node prev))
+                          |> not (after_perspective node entry) ?
+                              fold_entries update_start
+                                (fn entry1 as ((_, id1), _) => fn res =>
+                                  if after_perspective node entry1 then NONE
+                                  else SOME (new_exec state init id1 res)) node;
 
                         val node1 =
                           fold (fn (exec_id, (command_id, _)) => update_entry command_id exec_id)
@@ -468,6 +463,15 @@
                           |> set_last_exec last_exec
                           |> set_result result
                           |> set_touched false;
+
+                        val no_execs =
+                          fold_entries update_start
+                            (fn ((_, id0), exec0) => fn res =>
+                              if is_none exec0 then NONE
+                              else if is_some (lookup_entry node2 id0) then SOME res
+                              else SOME (id0 :: res)) node0 []
+                          handle Entries.UNDEFINED _ => [];
+
                       in ((no_execs, execs, [(name, node2)]), node2) end))
             end)
       |> Future.joins |> map #1;
@@ -511,8 +515,7 @@
             (singleton o Future.forks)
               {name = "theory:" ^ name, group = SOME (Future.new_group (SOME execution)),
                 deps = map (Future.task_of o #2) deps, pri = 1, interrupts = true}
-              (fold_entries NONE
-                (fn entry as (_, exec) => fn () => SOME (force_exec node exec)) node));
+              (fold_entries NONE (fn (_, exec) => fn () => SOME (force_exec node exec)) node));
 
     in (versions, commands, execs, execution) end);