src/Pure/PIDE/protocol.scala

   }
 
 
   /* execution */
 
-  def consolidate_execution(): Unit =
-    protocol_command("Document.consolidate_execution")
-
   def discontinue_execution(): Unit =
     protocol_command("Document.discontinue_execution")
 
   def cancel_exec(id: Document_ID.Exec): Unit =
     protocol_command("Document.cancel_exec", Document_ID(id))
 
 
   /* document versions */
 
   def update(old_id: Document_ID.Version, new_id: Document_ID.Version,
-    edits: List[Document.Edit_Command])
+    edits: List[Document.Edit_Command], consolidate: Boolean)
   {
     val edits_yxml =
     {
       import XML.Encode._
       def id: T[Command] = (cmd => long(cmd.id))

       {
         val (name, edit) = node_edit
         pair(string, encode_edit(name))(name.node, edit)
       })
       Symbol.encode_yxml(encode_edits(edits)) }
-    protocol_command("Document.update", Document_ID(old_id), Document_ID(new_id), edits_yxml)
+    protocol_command(
+      "Document.update", Document_ID(old_id), Document_ID(new_id), edits_yxml, consolidate.toString)
   }
 
   def remove_versions(versions: List[Document.Version])
   {
     val versions_yxml =