--- 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) =
--- 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))
--- 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