# HG changeset patch
# User wenzelm
# Date 1314990365 -7200
# Node ID 90bab3febb6caf2e019c4c8f97484e8e38439f6d
# Parent  665ebb45bc1aa1ba9870cc34fdc6a8e43d0c23b2
less agressive parsing of commands (priority ~1);
join commands just before actual assignment;

diff -r 665ebb45bc1a -r 90bab3febb6c src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Fri Sep 02 20:35:32 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Fri Sep 02 21:06:05 2011 +0200
@@ -25,7 +25,6 @@
   type state
   val init_state: state
   val define_command: command_id -> string -> string -> state -> state
-  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 ->
@@ -237,9 +236,7 @@
 
 abstype state = State of
  {versions: version Inttab.table,  (*version_id -> document content*)
-  commands:
-    (string * Toplevel.transition future) Inttab.table *  (*command_id -> name * transition*)
-    Toplevel.transition future list,  (*recent commands to be joined*)
+  commands: (string * Toplevel.transition future) Inttab.table,  (*command_id -> name * transition*)
   execs: (command_id * (Toplevel.state * unit lazy) lazy) Inttab.table,
     (*exec_id -> command_id with eval/print process*)
   execution: Future.group}  (*global execution process*)
@@ -253,7 +250,7 @@
 
 val init_state =
   make_state (Inttab.make [(no_id, empty_version)],
-    (Inttab.make [(no_id, (Toplevel.name_of Toplevel.empty, Future.value Toplevel.empty))], []),
+    Inttab.make [(no_id, (Toplevel.name_of Toplevel.empty, Future.value Toplevel.empty))],
     Inttab.make [(no_id, (no_id, Lazy.value (Toplevel.toplevel, no_print)))],
     Future.new_group NONE);
 
@@ -275,27 +272,26 @@
 (* commands *)
 
 fun define_command (id: command_id) name text =
-  map_state (fn (versions, (commands, recent), execs, execution) =>
+  map_state (fn (versions, commands, execs, execution) =>
     let
       val id_string = print_id id;
-      val tr =
-        Future.fork_pri 2 (fn () =>
-          Position.setmp_thread_data (Position.id_only id_string)
-            (fn () => Outer_Syntax.read_command (Position.id id_string) text) ());
+      val future =
+        (singleton o Future.forks)
+          {name = "Document.define_command", group = SOME (Future.new_group NONE),
+            deps = [], pri = ~1, interrupts = false}
+          (fn () =>
+            Position.setmp_thread_data (Position.id_only id_string)
+              (fn () => Outer_Syntax.read_command (Position.id id_string) text) ());
       val commands' =
-        Inttab.update_new (id, (name, tr)) commands
+        Inttab.update_new (id, (name, future)) commands
           handle Inttab.DUP dup => err_dup "command" dup;
-    in (versions, (commands', tr :: recent), execs, execution) end);
+    in (versions, commands', execs, execution) end);
 
 fun the_command (State {commands, ...}) (id: command_id) =
-  (case Inttab.lookup (#1 commands) id of
+  (case Inttab.lookup commands id of
     NONE => err_undef "command" id
   | SOME command => command);
 
-val join_commands =
-    map_state (fn (versions, (commands, recent), execs, execution) =>
-      (Future.join_results recent; (versions, (commands, []), execs, execution)));
-
 
 (* command executions *)
 
@@ -419,20 +415,16 @@
   if bad_init andalso is_none init then NONE
   else
     let
-      val (name, tr0) = the_command state command_id';
+      val (name, tr0) = the_command state command_id' ||> Future.join;
       val (modify_init, init') =
         if Keyword.is_theory_begin name then
           (Toplevel.modify_init (the_default illegal_init init), NONE)
         else (I, init);
-        val exec_id' = new_id ();
-      val exec' =
-        snd exec |> Lazy.map (fn (st, _) =>
-          let val tr =
-            Future.join tr0
-            |> modify_init
-            |> Toplevel.put_id (print_id exec_id');
-          in run_command tr st end)
-        |> pair command_id';
+      val exec_id' = new_id ();
+      val tr = tr0
+        |> modify_init
+        |> Toplevel.put_id (print_id exec_id');
+      val exec' = (command_id', Lazy.map (fn (st, _) => run_command tr st) (snd exec));
     in SOME ((exec_id', exec') :: execs, exec', init') end;
 
 fun make_required nodes =
diff -r 665ebb45bc1a -r 90bab3febb6c src/Pure/PIDE/isar_document.ML
--- a/src/Pure/PIDE/isar_document.ML	Fri Sep 02 20:35:32 2011 +0200
+++ b/src/Pure/PIDE/isar_document.ML	Fri Sep 02 21:06:05 2011 +0200
@@ -55,15 +55,14 @@
         val running = Document.cancel_execution state;
         val (assignment, state1) = Document.update old_id new_id edits state;
         val _ = Future.join_tasks running;
-        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 state3 = Document.execute new_id state2;
-      in state3 end));
+        val state2 = Document.execute new_id state1;
+      in state2 end));
 
 val _ =
   Isabelle_Process.add_command "Isar_Document.invoke_scala"