# HG changeset patch
# User wenzelm
# Date 1274987693 -7200
# Node ID d515609c88f794d06ba1b1ee52f968f87a7c311f
# Parent  0c0ef115c7aaf37cffdc8b5a4ad0b70f0f94cb49
substantial performance improvement by avoiding "re-ified" execution structure via future dependencies, instead use singleton execution (dummy future) that forces lazy state updates bottom-up;
tuned;

diff -r 0c0ef115c7aa -r d515609c88f7 src/Pure/Isar/isar_document.ML
--- a/src/Pure/Isar/isar_document.ML	Thu May 27 20:15:36 2010 +0200
+++ b/src/Pure/Isar/isar_document.ML	Thu May 27 21:14:53 2010 +0200
@@ -111,12 +111,10 @@
 
 (* states *)
 
-val empty_state = Future.value (SOME Toplevel.toplevel);
+val empty_state = Lazy.value (SOME Toplevel.toplevel);
 
 local
-
-val global_states = Unsynchronized.ref (Symtab.make [(no_id, empty_state)]);
-
+  val global_states = Unsynchronized.ref (Symtab.make [(no_id, empty_state)]);
 in
 
 fun define_state (id: state_id) =
@@ -139,9 +137,7 @@
 (* commands *)
 
 local
-
-val global_commands = Unsynchronized.ref (Symtab.make [(no_id, Toplevel.empty)]);
-
+  val global_commands = Unsynchronized.ref (Symtab.make [(no_id, Toplevel.empty)]);
 in
 
 fun define_command id tr =
@@ -160,9 +156,7 @@
 (* documents *)
 
 local
-
-val global_documents = Unsynchronized.ref (Symtab.empty: document Symtab.table);
-
+  val global_documents = Unsynchronized.ref (Symtab.empty: document Symtab.table);
 in
 
 fun define_document (id: document_id) document =
@@ -178,6 +172,18 @@
 end;
 
 
+(* execution *)
+
+local
+  val execution = Unsynchronized.ref (Future.value ());
+in
+
+fun execute e =
+  NAMED_CRITICAL "Isar" (fn () => (Future.cancel (! execution); execution := Future.fork e));
+
+end;
+
+
 
 (** main operations **)
 
@@ -198,9 +204,9 @@
       val end_state =
         the_state (the (#state (#3 (the
           (first_entry (fn (_, {next, ...}) => is_none next) document)))));
-      val _ =
-        Future.fork_deps [end_state] (fn () =>
-          (case Future.join end_state of
+      val _ =  (* FIXME regular execution (??) *)
+        Future.fork (fn () =>
+          (case Lazy.force end_state of
             SOME st =>
              (Toplevel.run_command name (Toplevel.put_id id (Toplevel.commit_exit Position.none)) st;
               ThyInfo.touch_child_thys name;
@@ -227,11 +233,11 @@
       let
         val state = the_state state_id;
         val state' =
-          Future.fork_deps [state] (fn () =>
-            (case Future.join state of
+          Lazy.lazy (fn () =>
+            (case Lazy.force state of
               NONE => NONE
             | SOME st => Toplevel.run_command name tr st));
-      in put_state state_id' state' end;
+      in put_state state_id' state'; state' end;
   in (state_id', ((id, state_id'), make_state') :: updates) end;
 
 fun report_updates updates =
@@ -248,19 +254,11 @@
       val new_document as Document {entries = new_entries, ...} = old_document
         |> fold (fn (id, SOME id2) => insert_after id id2 | (id, NONE) => delete_after id) edits;
 
-      fun cancel_old id = fold_entries id
-        (fn (_, {state = SOME state_id, ...}) => K (Future.cancel (the_state state_id)) | _ => K ())
-        old_document ();
-
       val (updates, new_document') =
         (case first_entry (is_changed old_entries) new_document of
-          NONE =>
-            (case first_entry (is_changed new_entries) old_document of
-              NONE => ([], new_document)
-            | SOME (_, id, _) => (cancel_old id; ([], new_document)))
+          NONE => ([], new_document)
         | SOME (prev, id, _) =>
             let
-              val _ = cancel_old id;
               val prev_state_id = the (#state (the_entry new_entries (the prev)));
               val (_, updates) = fold_entries id (new_state name) new_document (prev_state_id, []);
               val new_document' = new_document |> map_entries (fold (set_entry_state o #1) updates);
@@ -268,7 +266,8 @@
 
       val _ = define_document new_id new_document';
       val _ = report_updates (map #1 updates);
-      val _ = List.app (fn (_, run) => run ()) updates;
+      val execs = map (fn (_, make) => make ()) updates;
+      val _ = execute (fn () => List.app (ignore o Lazy.force) execs);
     in () end);
 
 end;