# HG changeset patch
# User wenzelm
# Date 1398374460 -7200
# Node ID ef3d00153e3b5c53cfc13918a7c42c7be215e77f
# Parent  8f102c18eab7a04e029fc4c9850c67546ec5ae1c
tuned signature;

diff -r 8f102c18eab7 -r ef3d00153e3b src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Thu Apr 24 23:13:17 2014 +0200
+++ b/src/Pure/PIDE/document.scala	Thu Apr 24 23:21:00 2014 +0200
@@ -608,12 +608,12 @@
     def tip_version: Version = history.tip.version.get_finished
 
     def continue_history(
-        previous: Future[Version],
-        edits: List[Edit_Text],
-        version: Future[Version]): (Change, State) =
+      previous: Future[Version],
+      edits: List[Edit_Text],
+      version: Future[Version]): State =
     {
       val change = Change.make(previous, edits, version)
-      (change, copy(history = history + change))
+      copy(history = history + change)
     }
 
     def prune_history(retain: Int = 0): (List[Version], State) =
diff -r 8f102c18eab7 -r ef3d00153e3b src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Thu Apr 24 23:13:17 2014 +0200
+++ b/src/Pure/PIDE/session.scala	Thu Apr 24 23:21:00 2014 +0200
@@ -345,7 +345,7 @@
 
       val previous = global_state.value.history.tip.version
       val version = Future.promise[Document.Version]
-      val change = global_state.change_result(_.continue_history(previous, edits, version))
+      global_state.change(_.continue_history(previous, edits, version))
 
       raw_edits.event(Session.Raw_Edits(doc_blobs, edits))
       change_parser.send(Text_Edits(previous, doc_blobs, edits, version))
diff -r 8f102c18eab7 -r ef3d00153e3b src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Thu Apr 24 23:13:17 2014 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Thu Apr 24 23:21:00 2014 +0200
@@ -36,7 +36,7 @@
     val nodes1 = nodes0 + (node_name -> nodes0(node_name).update_commands(Linear_Set(command)))
     val version1 = Document.Version.make(version0.syntax, nodes1)
     val state1 =
-      state0.continue_history(Future.value(version0), edits, Future.value(version1))._2
+      state0.continue_history(Future.value(version0), edits, Future.value(version1))
         .define_version(version1, state0.the_assignment(version0))
         .assign(version1.id, List(command.id -> List(Document_ID.make())))._2