tuned;

--- a/src/Pure/PIDE/session.scala	Tue Apr 29 22:52:15 2014 +0200
+++ b/src/Pure/PIDE/session.scala	Wed Apr 30 12:12:44 2014 +0200
@@ -8,7 +8,6 @@
 package isabelle
 
 
-import scala.collection.mutable
 import scala.collection.immutable.Queue
 
 
@@ -95,7 +94,6 @@
   }
 
 
-
   /* protocol handlers */
 
   abstract class Protocol_Handler
@@ -201,31 +199,18 @@
 
 
 
-  /** pipelined change parsing **/
+  /** main protocol manager **/
 
-  private case class Text_Edits(
-    previous: Future[Document.Version],
-    doc_blobs: Document.Blobs,
-    text_edits: List[Document.Edit_Text],
-    version_result: Promise[Document.Version])
+  /* internal messages */
 
-  private val change_parser = Consumer_Thread.fork[Text_Edits]("change_parser", daemon = true)
-  {
-    case Text_Edits(previous, doc_blobs, text_edits, version_result) =>
-      val prev = previous.get_finished
-      val change =
-        Timing.timeit("parse_change", timing) {
-          resources.parse_change(reparse_limit, prev, doc_blobs, text_edits)
-        }
-      version_result.fulfill(change.version)
-      manager.send(change)
-      true
-  }
+  private case class Start(name: String, args: List[String])
+  private case object Stop
+  private case class Cancel_Exec(exec_id: Document_ID.Exec)
+  private case class Protocol_Command(name: String, args: List[String])
+  private case class Update_Options(options: Options)
+  private case object Prune_History
 
 
-
-  /** main protocol manager **/
-
   /* global state */
 
   private val syslog = new Session.Syslog(syslog_limit)
@@ -249,10 +234,6 @@
     version.syntax getOrElse resources.base_syntax
   }
 
-  def snapshot(name: Document.Node.Name = Document.Node.Name.empty,
-      pending_edits: List[Text.Edit] = Nil): Document.Snapshot =
-    global_state.value.snapshot(name, pending_edits)
-
 
   /* protocol handlers */
 
@@ -274,14 +255,26 @@
   }
 
 
-  /* internal messages */
+  /* pipelined change parsing */
+
+  private case class Text_Edits(
+    previous: Future[Document.Version],
+    doc_blobs: Document.Blobs,
+    text_edits: List[Document.Edit_Text],
+    version_result: Promise[Document.Version])
 
-  private case class Start(name: String, args: List[String])
-  private case object Stop
-  private case class Cancel_Exec(exec_id: Document_ID.Exec)
-  private case class Protocol_Command(name: String, args: List[String])
-  private case class Update_Options(options: Options)
-  private case object Prune_History
+  private val change_parser = Consumer_Thread.fork[Text_Edits]("change_parser", daemon = true)
+  {
+    case Text_Edits(previous, doc_blobs, text_edits, version_result) =>
+      val prev = previous.get_finished
+      val change =
+        Timing.timeit("parse_change", timing) {
+          resources.parse_change(reparse_limit, prev, doc_blobs, text_edits)
+        }
+      version_result.fulfill(change.version)
+      manager.send(change)
+      true
+  }
 
 
   /* buffered changes */
@@ -573,7 +566,11 @@
   }
 
 
-  /* actions */
+  /* main operations */
+
+  def snapshot(name: Document.Node.Name = Document.Node.Name.empty,
+      pending_edits: List[Text.Edit] = Nil): Document.Snapshot =
+    global_state.value.snapshot(name, pending_edits)
 
   def start(name: String, args: List[String])
   { manager.send(Start(name, args)) }