# HG changeset patch
# User wenzelm
# Date 1281038198 -7200
# Node ID 5c82435803341a23c39d452a5696f7c06811264f
# Parent  e669779bb8c4cb669dc50ca0d574d6ff02dd6403
misc tuning -- produce reverse_edits at most once (note that foldRight produces a reversed list internally, while recursion is infisible due to small stack vs. large stack frames on JVM);

diff -r e669779bb8c4 -r 5c8243580334 src/Pure/PIDE/change.scala
--- a/src/Pure/PIDE/change.scala	Thu Aug 05 21:40:20 2010 +0200
+++ b/src/Pure/PIDE/change.scala	Thu Aug 05 21:56:38 2010 +0200
@@ -65,17 +65,20 @@
   def snapshot(name: String, extra_edits: List[Text_Edit]): Change.Snapshot =
   {
     val latest = this
-    val stable = latest.ancestors.find(_.is_assigned).get
-    val changes =
-      (extra_edits /: latest.ancestors.takeWhile(_ != stable))((edits, change) =>
+    val stable = latest.ancestors.find(_.is_assigned)
+    require(stable.isDefined)
+
+    val edits =
+      (extra_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.join_document
+      val document = stable.get.join_document
       val node = document.nodes(name)
-      val is_outdated = !(extra_edits.isEmpty && latest == stable)
-      def convert(offset: Int): Int = (offset /: changes)((i, change) => change.convert(i))
-      def revert(offset: Int): Int = (offset /: changes.reverse)((i, change) => change.revert(i))  // FIXME fold_rev (!?)
+      val is_outdated = !(extra_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))
     }
   }
 }
\ No newline at end of file