# HG changeset patch
# User wenzelm
# Date 1281192543 -7200
# Node ID ee0f46c45c19c66b4f4f7dabd7a1558b7dc63bfb
# Parent  809578d7f6af1a56cdd98c2d669c8e15a84cdc90
tuned;

diff -r 809578d7f6af -r ee0f46c45c19 src/Pure/PIDE/change.scala
--- a/src/Pure/PIDE/change.scala	Sat Aug 07 16:44:52 2010 +0200
+++ b/src/Pure/PIDE/change.scala	Sat Aug 07 16:49:03 2010 +0200
@@ -50,21 +50,21 @@
 
   /* snapshot */
 
-  def snapshot(name: String, extra_edits: List[Text_Edit]): Change.Snapshot =
+  def snapshot(name: String, pending_edits: List[Text_Edit]): Change.Snapshot =
   {
     val latest = this
     val stable = latest.ancestors.find(_.is_assigned)
     require(stable.isDefined)
 
     val edits =
-      (extra_edits /: latest.ancestors.takeWhile(_ != stable.get))((edits, change) =>
+      (pending_edits /: latest.ancestors.takeWhile(_ != stable.get))((edits, change) =>
           (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits)
     lazy val reverse_edits = edits.reverse
 
     new Change.Snapshot {
       val document = stable.get.join_document
       val node = document.nodes(name)
-      val is_outdated = !(extra_edits.isEmpty && latest == stable.get)
+      val is_outdated = !(pending_edits.isEmpty && latest == stable.get)
       def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i))
       def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i))
     }
diff -r 809578d7f6af -r ee0f46c45c19 src/Tools/jEdit/src/jedit/document_model.scala
--- a/src/Tools/jEdit/src/jedit/document_model.scala	Sat Aug 07 16:44:52 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Sat Aug 07 16:49:03 2010 +0200
@@ -262,6 +262,7 @@
       val start = buffer.getLineStartOffset(line)
       val stop = start + line_segment.count
 
+      // FIXME proper synchronization / thread context (!??)
       val snapshot = Swing_Thread.now { Document_Model.this.snapshot() }
 
       /* FIXME