# HG changeset patch
# User wenzelm
# Date 1285415854 -7200
# Node ID 625a3bc4417b3bf8d81aa0765d04f856e3597b61
# Parent  d54242927fb168556e82300ad31605edd9958bd0
tuned signature;

diff -r d54242927fb1 -r 625a3bc4417b src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Fri Sep 24 21:05:07 2010 +0200
+++ b/src/Pure/PIDE/document.scala	Sat Sep 25 13:57:34 2010 +0200
@@ -136,8 +136,8 @@
     val edits: List[Node_Text_Edit],
     val result: Future[(List[Edit[Command]], Version)])
   {
-    val current: Future[Version] = result.map(_._2)
-    def is_finished: Boolean = previous.is_finished && current.is_finished
+    val version: Future[Version] = result.map(_._2)
+    def is_finished: Boolean = previous.is_finished && version.is_finished
   }
 
 
@@ -279,7 +279,7 @@
     def snapshot(name: String, pending_edits: List[Text.Edit]): Snapshot =
     {
       val found_stable = history.undo_list.find(change =>
-        change.is_finished && is_assigned(change.current.get_finished))
+        change.is_finished && is_assigned(change.version.get_finished))
       require(found_stable.isDefined)
       val stable = found_stable.get
       val latest = history.undo_list.head
@@ -291,7 +291,7 @@
 
       new Snapshot
       {
-        val version = stable.current.get_finished
+        val version = stable.version.get_finished
         val node = version.nodes(name)
         val is_outdated = !(pending_edits.isEmpty && latest == stable)
 
diff -r d54242927fb1 -r 625a3bc4417b src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Fri Sep 24 21:05:07 2010 +0200
+++ b/src/Pure/System/session.scala	Sat Sep 25 13:57:34 2010 +0200
@@ -149,7 +149,7 @@
     //{{{
     {
       val previous = change.previous.get_finished
-      val (node_edits, current) = change.result.get_finished
+      val (node_edits, version) = change.result.get_finished
 
       var former_assignment = global_state.peek().the_assignment(previous).get_finished
       for {
@@ -180,8 +180,8 @@
               }
             (name -> Some(ids))
         }
-      global_state.change(_.define_version(current, former_assignment))
-      prover.edit_version(previous.id, current.id, id_edits)
+      global_state.change(_.define_version(version, former_assignment))
+      prover.edit_version(previous.id, version.id, id_edits)
     }
     //}}}
 
@@ -241,12 +241,12 @@
           if (prover != null) prover.interrupt
 
         case Edit_Version(edits) if prover != null =>
-          val previous = global_state.peek().history.tip.current
+          val previous = global_state.peek().history.tip.version
           val result = Future.fork { Thy_Syntax.text_edits(Session.this, previous.join, edits) }
           val change = global_state.change_yield(_.extend_history(previous, edits, result))
 
           val this_actor = self
-          change.current.map(_ => {
+          change.version.map(_ => {
             assignments.await { global_state.peek().is_assigned(previous.get_finished) }
             this_actor ! change })