src/Pure/PIDE/session.scala

--- a/src/Pure/PIDE/session.scala	Sat Mar 29 09:34:51 2014 +0100
+++ b/src/Pure/PIDE/session.scala	Sat Mar 29 10:17:09 2014 +0100
@@ -18,6 +18,16 @@
 
 object Session
 {
+  /* change */
+
+  sealed case class Change(
+    previous: Document.Version,
+    doc_blobs: Document.Blobs,
+    syntax_changed: Boolean,
+    doc_edits: List[Document.Edit_Command],
+    version: Document.Version)
+
+
   /* events */
 
   //{{{
@@ -179,12 +189,12 @@
 
         case Text_Edits(previous, doc_blobs, text_edits, version_result) =>
           val prev = previous.get_finished
-          val (syntax_changed, doc_edits, version) =
-            Timing.timeit("text_edits", timing) {
-              resources.text_edits(reparse_limit, prev, doc_blobs, text_edits)
+          val change =
+            Timing.timeit("parse_edits", timing) {
+              resources.parse_edits(reparse_limit, prev, doc_blobs, text_edits)
             }
-          version_result.fulfill(version)
-          sender ! Change(doc_blobs, syntax_changed, doc_edits, prev, version)
+          version_result.fulfill(change.version)
+          sender ! change
 
         case bad => System.err.println("change_parser: ignoring bad message " + bad)
       }
@@ -249,12 +259,6 @@
 
   private case class Start(args: List[String])
   private case class Cancel_Exec(exec_id: Document_ID.Exec)
-  private case class Change(
-    doc_blobs: Document.Blobs,
-    syntax_changed: Boolean,
-    doc_edits: List[Document.Edit_Command],
-    previous: Document.Version,
-    version: Document.Version)
   private case class Protocol_Command(name: String, args: List[String])
   private case class Messages(msgs: List[Isabelle_Process.Message])
   private case class Update_Options(options: Options)
@@ -367,18 +371,16 @@
 
     /* resulting changes */
 
-    def handle_change(change: Change)
+    def handle_change(change: Session.Change)
     //{{{
     {
-      val Change(doc_blobs, syntax_changed, doc_edits, previous, version) = change
-
       def id_command(command: Command)
       {
         for {
           digest <- command.blobs_digests
           if !global_state().defined_blob(digest)
         } {
-          doc_blobs.get(digest) match {
+          change.doc_blobs.get(digest) match {
             case Some(blob) =>
               global_state >> (_.define_blob(digest))
               prover.get.define_blob(blob)
@@ -392,16 +394,16 @@
           prover.get.define_command(command)
         }
       }
-      doc_edits foreach {
+      change.doc_edits foreach {
         case (_, edit) =>
           edit foreach { case (c1, c2) => c1 foreach id_command; c2 foreach id_command }
       }
 
-      val assignment = global_state().the_assignment(previous).check_finished
-      global_state >> (_.define_version(version, assignment))
-      prover.get.update(previous.id, version.id, doc_edits)
+      val assignment = global_state().the_assignment(change.previous).check_finished
+      global_state >> (_.define_version(change.version, assignment))
+      prover.get.update(change.previous.id, change.version.id, change.doc_edits)
 
-      if (syntax_changed) resources.syntax_changed()
+      if (change.syntax_changed) resources.syntax_changed()
     }
     //}}}
 
@@ -556,11 +558,11 @@
               all_messages.event(output)
           }
 
-        case change: Change
+        case change: Session.Change
         if prover.isDefined && global_state().is_assigned(change.previous) =>
           handle_change(change)
 
-        case bad if !bad.isInstanceOf[Change] =>
+        case bad if !bad.isInstanceOf[Session.Change] =>
           System.err.println("session_actor: ignoring bad message " + bad)
       }
     }