refined define_command vs. run_command: static tokenization vs. dynamic parsing, to increase the chance that the proper transaction is run after redefining commands (NB: requires slightly more space and time for document state);

--- a/src/Pure/Isar/outer_syntax.ML	Mon Mar 12 16:04:00 2012 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Mon Mar 12 17:27:52 2012 +0100
@@ -34,7 +34,7 @@
   val process_file: Path.T -> theory -> theory
   type isar
   val isar: TextIO.instream -> bool -> isar
-  val read_command: Position.T -> string -> Toplevel.transition
+  val read_span: outer_syntax -> Token.T list -> Toplevel.transition * bool
   val read_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.element ->
     (Toplevel.transition * Toplevel.transition list) list
 end;
@@ -270,12 +270,6 @@
     handle ERROR msg => (Toplevel.malformed range_pos msg, true)
   end;
 
-fun read_command pos str =
-  let
-    val (lexs, outer_syntax) = get_syntax ();
-    val toks = Thy_Syntax.parse_tokens lexs pos str;
-  in #1 (read_span outer_syntax toks) end;
-
 fun read_element outer_syntax init {head, proof, proper_proof} =
   let
     val read = read_span outer_syntax o Thy_Syntax.span_content;

--- a/src/Pure/PIDE/document.ML	Mon Mar 12 16:04:00 2012 +0100
+++ b/src/Pure/PIDE/document.ML	Mon Mar 12 17:27:52 2012 +0100
@@ -240,7 +240,7 @@
 
 abstype state = State of
  {versions: version Inttab.table,  (*version_id -> document content*)
-  commands: (string * Toplevel.transition future) Inttab.table,  (*command_id -> name * transition*)
+  commands: (string * Token.T list future) Inttab.table,  (*command_id -> name * span*)
   execution: version_id * Future.group}  (*current execution process*)
 with
 
@@ -273,17 +273,18 @@
 
 (* commands *)
 
+fun tokenize_command id text =
+  Position.setmp_thread_data (Position.id_only id)
+    (fn () => Thy_Syntax.parse_tokens (#1 (Outer_Syntax.get_syntax ())) (Position.id id) text) ();
+
 fun define_command (id: command_id) name text =
   map_state (fn (versions, commands, execution) =>
     let
-      val id_string = print_id id;
       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) ());
+          (fn () => tokenize_command (print_id id) text);
       val commands' =
         Inttab.update_new (id, (name, future)) commands
           handle Inttab.DUP dup => err_dup "command" dup;
@@ -408,16 +409,20 @@
   if bad_init andalso is_none init then NONE
   else
     let
-      val (name, tr0) = the_command state command_id' ||> Future.join;
+      val (name, span) = 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 tr = tr0
-        |> modify_init
-        |> Toplevel.put_id (print_id exec_id');
-      val exec' = snd (snd command_exec) |> Lazy.map (fn (st, _) => run_command tr st);
+      val exec_id'_string = print_id exec_id';
+      val tr =
+        Position.setmp_thread_data (Position.id_only exec_id'_string)
+          (fn () =>
+            #1 (Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) span)
+            |> modify_init
+            |> Toplevel.put_id exec_id'_string);
+      val exec' = snd (snd command_exec) |> Lazy.map (fn (st, _) => run_command (tr ()) st);
       val command_exec' = (command_id', (exec_id', exec'));
     in SOME (command_exec' :: execs, command_exec', init') end;