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