apply all text edits to each node, before determining the resulting doc_edits -- allow several iterations to consolidate spans etc.;
expand Clear edit before sending to prover;
at most one full reparse of each node;

--- a/src/Pure/PIDE/document.ML	Fri Aug 10 13:33:07 2012 +0200
+++ b/src/Pure/PIDE/document.ML	Fri Aug 10 15:14:45 2012 +0200
@@ -17,7 +17,7 @@
   val print_id: id -> string
   type node_header = string * Thy_Header.header * string list
   datatype node_edit =
-    Clear |
+    Clear |    (* FIXME unused !? *)
     Edits of (command_id option * command_id option) list |
     Deps of node_header |
     Perspective of command_id list

--- a/src/Pure/PIDE/protocol.ML	Fri Aug 10 13:33:07 2012 +0200
+++ b/src/Pure/PIDE/protocol.ML	Fri Aug 10 15:14:45 2012 +0200
@@ -33,7 +33,7 @@
             let open XML.Decode in
               list (pair string
                 (variant
-                 [fn ([], []) => Document.Clear,
+                 [fn ([], []) => Document.Clear,  (* FIXME unused !? *)
                   fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
                   fn ([], a) =>
                     let

--- a/src/Pure/PIDE/protocol.scala	Fri Aug 10 13:33:07 2012 +0200
+++ b/src/Pure/PIDE/protocol.scala	Fri Aug 10 15:14:45 2012 +0200
@@ -213,7 +213,7 @@
       def encode_edit(name: Document.Node.Name)
           : T[Document.Node.Edit[(Option[Command], Option[Command]), Command.Perspective]] =
         variant(List(
-          { case Document.Node.Clear() => (Nil, Nil) },
+          { case Document.Node.Clear() => (Nil, Nil) },  // FIXME unused !?
           { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
           { case Document.Node.Deps(header) =>
               val dir = Isabelle_System.posix_path(name.dir)

--- a/src/Pure/System/session.scala	Fri Aug 10 13:33:07 2012 +0200
+++ b/src/Pure/System/session.scala	Fri Aug 10 15:14:45 2012 +0200
@@ -453,7 +453,7 @@
     header: Document.Node.Header, perspective: Text.Perspective, text: String)
   {
     edit(List(header_edit(name, header),
-      name -> Document.Node.Clear(),    // FIXME diff wrt. existing node
+      name -> Document.Node.Clear(),
       name -> Document.Node.Edits(List(Text.Edit.insert(0, text))),
       name -> Document.Node.Perspective(perspective)))
   }

--- a/src/Pure/Thy/thy_syntax.scala	Fri Aug 10 13:33:07 2012 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Fri Aug 10 15:14:45 2012 +0200
@@ -165,7 +165,7 @@
 
   /** text edits **/
 
-  /* phase 1: edit individual command source */
+  /* edit individual command source */
 
   @tailrec private def edit_text(eds: List[Text.Edit], commands: Linear_Set[Command])
       : Linear_Set[Command] =
@@ -194,7 +194,7 @@
   }
 
 
-  /* phase 2a: reparse range of command spans */
+  /* reparse range of command spans */
 
   @tailrec private def chop_common(
       cmds: List[Command], spans: List[Command.Span]): (List[Command], List[Command.Span]) =
@@ -230,8 +230,9 @@
   }
 
 
-  /* phase 2b: recover command spans after edits */
+  /* recover command spans after edits */
 
+  // FIXME somewhat slow
   private def recover_spans(
     syntax: Outer_Syntax,
     name: Document.Node.Name,
@@ -256,7 +257,7 @@
   }
 
 
-  /* phase 2c: consolidate unfinished spans */
+  /* consolidate unfinished spans */
 
   private def consolidate_spans(
     syntax: Outer_Syntax,
@@ -280,7 +281,7 @@
   }
 
 
-  /* main phase */
+  /* main */
 
   private def diff_commands(old_cmds: Linear_Set[Command], new_cmds: Linear_Set[Command])
     : List[(Option[Command], Option[Command])] =
@@ -292,6 +293,29 @@
     inserted.map(cmd => (new_cmds.prev(cmd), Some(cmd)))
   }
 
+  private def text_edit(syntax: Outer_Syntax,
+    node: Document.Node, edit: Document.Edit_Text): Document.Node =
+  {
+    edit match {
+      case (_, Document.Node.Clear()) => node.clear
+
+      case (name, Document.Node.Edits(text_edits)) =>
+        val commands0 = node.commands
+        val commands1 = edit_text(text_edits, commands0)
+        val commands2 = recover_spans(syntax, name, node.perspective, commands1)
+        node.update_commands(commands2)
+
+      case (_, Document.Node.Deps(_)) => node
+
+      case (name, Document.Node.Perspective(text_perspective)) =>
+        val perspective = command_perspective(node, text_perspective)
+        if (node.perspective same perspective) node
+        else
+          node.update_perspective(perspective)
+            .update_commands(consolidate_spans(syntax, name, perspective, node.commands))
+    }
+  }
+
   def text_edits(
       base_syntax: Outer_Syntax,
       previous: Document.Version,
@@ -304,38 +328,27 @@
     var nodes = nodes0
     val doc_edits = new mutable.ListBuffer[Document.Edit_Command]; doc_edits ++= doc_edits0
 
-    (edits ::: reparse.map((_, Document.Node.Edits(Nil)))) foreach {
-      case (name, Document.Node.Clear()) =>
-        doc_edits += (name -> Document.Node.Clear())
-        nodes += (name -> nodes(name).clear)
-
-      case (name, Document.Node.Edits(text_edits)) =>
-        val node = nodes(name)
+    val node_edits =
+      (edits ::: reparse.map((_, Document.Node.Edits(Nil)))).groupBy(_._1)
+        .asInstanceOf[Map[Document.Node.Name, List[Document.Edit_Text]]]  // FIXME ???
 
-        val commands0 = node.commands
-        val commands1 = edit_text(text_edits, commands0)
-        val commands2 = recover_spans(syntax, name, node.perspective, commands1)   // FIXME somewhat slow
-        val commands3 =
-          if (reparse_set.contains(name) && !commands2.isEmpty)
-            reparse_spans(syntax, name, commands2, commands2.head, commands2.last)  // FIXME somewhat slow
-          else commands2
+    node_edits foreach {
+      case (name, edits) =>
+        val node = nodes(name)
+        val commands = node.commands
 
-        doc_edits += (name -> Document.Node.Edits(diff_commands(commands0, commands3)))
-        nodes += (name -> node.update_commands(commands3))
-
-      case (name, Document.Node.Deps(_)) =>
+        val node1 =
+          if (reparse_set(name) && !commands.isEmpty)
+            node.update_commands(reparse_spans(syntax, name, commands, commands.head, commands.last))
+          else node
+        val node2 = (node1 /: edits)(text_edit(syntax, _, _))
 
-      case (name, Document.Node.Perspective(text_perspective)) =>
-        val node = nodes(name)
-        val perspective = command_perspective(node, text_perspective)
-        if (!(node.perspective same perspective)) {
-/* FIXME
-          val commands1 = consolidate_spans(syntax, name, perspective, node.commands)
-          doc_edits += (name -> Document.Node.Edits(diff_commands(node.commands, commands1)))
-*/
-          doc_edits += (name -> Document.Node.Perspective(perspective))
-          nodes += (name -> node.update_perspective(perspective))
-        }
+        if (!(node.perspective same node2.perspective))
+          doc_edits += (name -> Document.Node.Perspective(node2.perspective))
+
+        doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node2.commands)))
+
+        nodes += (name -> node2)
     }
 
     (doc_edits.toList, Document.Version.make(syntax, nodes))