# HG changeset patch
# User wenzelm
# Date 1396084629 -3600
# Node ID c20053f670936474386c389ea0672e93ad79ae55
# Parent  9a513737a0b2b4a726a20db500ab1136f4c2a743
tuned signature;

diff -r 9a513737a0b2 -r c20053f67093 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Sat Mar 29 09:34:51 2014 +0100
+++ b/src/Pure/PIDE/resources.scala	Sat Mar 29 10:17:09 2014 +0100
@@ -93,12 +93,12 @@
 
   /* theory text edits */
 
-  def text_edits(
-    reparse_limit: Int,
-    previous: Document.Version,
-    doc_blobs: Document.Blobs,
-    edits: List[Document.Edit_Text]): (Boolean, List[Document.Edit_Command], Document.Version) =
-    Thy_Syntax.text_edits(this, reparse_limit, previous, doc_blobs, edits)
+  def parse_edits(
+      reparse_limit: Int,
+      previous: Document.Version,
+      doc_blobs: Document.Blobs,
+      edits: List[Document.Edit_Text]): Session.Change =
+    Thy_Syntax.parse_edits(this, reparse_limit, previous, doc_blobs, edits)
 
   def syntax_changed() { }
 }
diff -r 9a513737a0b2 -r c20053f67093 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)
       }
     }
diff -r 9a513737a0b2 -r c20053f67093 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Sat Mar 29 09:34:51 2014 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Sat Mar 29 10:17:09 2014 +0100
@@ -431,19 +431,18 @@
     }
   }
 
-  def text_edits(
+  def parse_edits(
       resources: Resources,
       reparse_limit: Int,
       previous: Document.Version,
       doc_blobs: Document.Blobs,
-      edits: List[Document.Edit_Text])
-    : (Boolean, List[Document.Edit_Command], Document.Version) =
+      edits: List[Document.Edit_Text]): Session.Change =
   {
     val ((syntax, syntax_changed), reparse0, nodes0, doc_edits0) =
       header_edits(resources.base_syntax, previous, edits)
 
     if (edits.isEmpty)
-      (false, Nil, Document.Version.make(syntax, previous.nodes))
+      Session.Change(previous, doc_blobs, false, Nil, Document.Version.make(syntax, previous.nodes))
     else {
       val reparse =
         (reparse0 /: nodes0.entries)({
@@ -482,7 +481,12 @@
           nodes += (name -> node2)
       }
 
-      (syntax_changed, doc_edits.toList, Document.Version.make(syntax, nodes))
+      Session.Change(
+        previous,
+        doc_blobs,
+        syntax_changed,
+        doc_edits.toList,
+        Document.Version.make(syntax, nodes))
     }
   }
 }