# HG changeset patch
# User wenzelm
# Date 1314813133 -7200
# Node ID 49657380fba6af6109b6a1dbbc841f75a572bff0
# Parent  6ec4a5eb2fc0ac25c7105f680e17924ee0ebb6f9
tuned join_commands: avoid traversing cumulative table;

diff -r 6ec4a5eb2fc0 -r 49657380fba6 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Wed Aug 31 17:36:10 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Wed Aug 31 19:52:13 2011 +0200
@@ -25,7 +25,7 @@
   type state
   val init_state: state
   val define_command: command_id -> string -> state -> state
-  val join_commands: state -> unit
+  val join_commands: state -> state
   val cancel_execution: state -> Future.task list
   val update_perspective: version_id -> version_id -> string -> command_id list -> state -> state
   val update: version_id -> version_id -> edit list -> state ->
@@ -230,7 +230,9 @@
 
 abstype state = State of
  {versions: version Inttab.table,  (*version_id -> document content*)
-  commands: Toplevel.transition future Inttab.table,  (*command_id -> transition (future parsing)*)
+  commands:
+    Toplevel.transition future Inttab.table *  (*command_id -> transition (future parsing)*)
+    Toplevel.transition future list,  (*recent commands to be joined*)
   execs: (command_id * (Toplevel.state * unit lazy) lazy) Inttab.table,
     (*exec_id -> command_id with eval/print process*)
   execution: Future.group}  (*global execution process*)
@@ -244,7 +246,7 @@
 
 val init_state =
   make_state (Inttab.make [(no_id, empty_version)],
-    Inttab.make [(no_id, Future.value Toplevel.empty)],
+    (Inttab.make [(no_id, Future.value Toplevel.empty)], []),
     Inttab.make [(no_id, (no_id, Lazy.value (Toplevel.toplevel, no_print)))],
     Future.new_group NONE);
 
@@ -266,7 +268,7 @@
 (* commands *)
 
 fun define_command (id: command_id) text =
-  map_state (fn (versions, commands, execs, execution) =>
+  map_state (fn (versions, (commands, recent), execs, execution) =>
     let
       val id_string = print_id id;
       val tr =
@@ -276,15 +278,16 @@
       val commands' =
         Inttab.update_new (id, tr) commands
           handle Inttab.DUP dup => err_dup "command" dup;
-    in (versions, commands', execs, execution) end);
+    in (versions, (commands', tr :: recent), execs, execution) end);
 
 fun the_command (State {commands, ...}) (id: command_id) =
-  (case Inttab.lookup commands id of
+  (case Inttab.lookup (#1 commands) id of
     NONE => err_undef "command" id
   | SOME tr => tr);
 
-fun join_commands (State {commands, ...}) =
-  Inttab.fold (fn (_, tr) => fn () => ignore (Future.join_result tr)) commands ();
+val join_commands =
+    map_state (fn (versions, (commands, recent), execs, execution) =>
+      (Future.join_results recent; (versions, (commands, []), execs, execution)));
 
 
 (* command executions *)
diff -r 6ec4a5eb2fc0 -r 49657380fba6 src/Pure/PIDE/isar_document.ML
--- a/src/Pure/PIDE/isar_document.ML	Wed Aug 31 17:36:10 2011 +0200
+++ b/src/Pure/PIDE/isar_document.ML	Wed Aug 31 19:52:13 2011 +0200
@@ -48,17 +48,17 @@
             end;
 
         val running = Document.cancel_execution state;
-        val (assignment, state') = Document.update old_id new_id edits state;
+        val (assignment, state1) = Document.update old_id new_id edits state;
         val _ = Future.join_tasks running;
-        val _ = Document.join_commands state';
+        val state2 = Document.join_commands state1;
         val _ =
           Output.status (Markup.markup (Markup.assign new_id)
             (assignment |>
               let open XML.Encode
               in pair (list (pair int (option int))) (list (pair string (option int))) end
               |> YXML.string_of_body));
-        val state'' = Document.execute new_id state';
-      in state'' end));
+        val state3 = Document.execute new_id state2;
+      in state3 end));
 
 val _ =
   Isabelle_Process.add_command "Isar_Document.invoke_scala"