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