# HG changeset patch
# User wenzelm
# Date 1281024037 -7200
# Node ID eab0d1c2e46ed19bc46272119a95e7c134b8aad2
# Parent  2837c952ca3142a693814d75427702d51c649691
Change.Snapshot: include from_current/to_current here, with precomputed changes;

diff -r 2837c952ca31 -r eab0d1c2e46e src/Pure/PIDE/change.scala
--- a/src/Pure/PIDE/change.scala	Thu Aug 05 16:58:18 2010 +0200
+++ b/src/Pure/PIDE/change.scala	Thu Aug 05 18:00:37 2010 +0200
@@ -14,11 +14,11 @@
 
   abstract class Snapshot
   {
-    val latest_version: Change
-    val stable_version: Change
     val document: Document
     val node: Document.Node
-    def is_outdated: Boolean = stable_version != latest_version
+    val is_outdated: Boolean
+    def from_current(offset: Int): Int
+    def to_current(offset: Int): Int
   }
 }
 
@@ -62,14 +62,22 @@
 
   /* snapshot */
 
-  def snapshot(name: String): Change.Snapshot =
+  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) =>
+          (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits)
+
     new Change.Snapshot {
-      val latest_version = latest
-      val stable_version: Change = latest.ancestors.find(_.is_assigned).get
-      val document: Document = stable_version.join_document
-      val node: Document.Node = document.nodes(name)
+      val document = stable.join_document
+      val node = document.nodes(name)
+      val is_outdated = !(extra_edits.isEmpty && latest == stable)
+      def from_current(offset: Int): Int =
+        (offset /: changes.reverse)((i, change) => change before i)  // FIXME fold_rev (!?)
+      def to_current(offset: Int): Int =
+        (offset /: changes)((i, change) => change after i)
     }
   }
 }
\ No newline at end of file
diff -r 2837c952ca31 -r eab0d1c2e46e src/Tools/jEdit/src/jedit/document_model.scala
--- a/src/Tools/jEdit/src/jedit/document_model.scala	Thu Aug 05 16:58:18 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Thu Aug 05 18:00:37 2010 +0200
@@ -70,41 +70,26 @@
   }
 
 
-  /* history */
+  /* global state -- owned by Swing thread */
+
+  @volatile private var history = Change.init // owned by Swing thread
+  private val edits_buffer = new mutable.ListBuffer[Text_Edit]   // owned by Swing thread
+
+
+  /* snapshot */
 
   // FIXME proper error handling
   val thy_name = Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath))._2
 
-  @volatile private var history = Change.init // owned by Swing thread
-
-  def current_change(): Change = history
-  def snapshot(): Change.Snapshot = current_change().snapshot(thy_name)
-
-
-  /* transforming offsets */
-
-  private def changes_from(doc: Document): List[Text_Edit] =
-  {
-    Swing_Thread.assert()
-    (edits_buffer.toList /:
-      current_change.ancestors.takeWhile(_.id != doc.id))((edits, change) =>
-        (for ((name, eds) <- change.edits if name == thy_name) yield eds).flatten ::: edits)
-  }
-
-  def from_current(doc: Document, offset: Int): Int =
-    (offset /: changes_from(doc).reverse) ((i, change) => change before i)
-
-  def to_current(doc: Document, offset: Int): Int =
-    (offset /: changes_from(doc)) ((i, change) => change after i)
+  def snapshot(): Change.Snapshot =
+    Swing_Thread.now { history.snapshot(thy_name, edits_buffer.toList) }
 
 
   /* text edits */
 
-  private val edits_buffer = new mutable.ListBuffer[Text_Edit]   // owned by Swing thread
-
   private val edits_delay = Swing_Thread.delay_last(session.input_delay) {
     if (!edits_buffer.isEmpty) {
-      val new_change = current_change().edit(session, List((thy_name, edits_buffer.toList)))
+      val new_change = history.edit(session, List((thy_name, edits_buffer.toList)))
       edits_buffer.clear
       history = new_change
       new_change.result.map(_ => session.input(new_change))
diff -r 2837c952ca31 -r eab0d1c2e46e src/Tools/jEdit/src/jedit/document_view.scala
--- a/src/Tools/jEdit/src/jedit/document_view.scala	Thu Aug 05 16:58:18 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Thu Aug 05 18:00:37 2010 +0200
@@ -120,16 +120,14 @@
   {
     Swing_Thread.assert()
 
-    val document = snapshot.document
-    val doc = snapshot.node
     val buffer = model.buffer
     var visible_change = false
 
-    for ((command, start) <- doc.command_starts) {
+    for ((command, start) <- snapshot.node.command_starts) {
       if (changed(command)) {
         val stop = start + command.length
-        val line1 = buffer.getLineOfOffset(model.to_current(document, start))
-        val line2 = buffer.getLineOfOffset(model.to_current(document, stop))
+        val line1 = buffer.getLineOfOffset(snapshot.to_current(start))
+        val line2 = buffer.getLineOfOffset(snapshot.to_current(stop))
         if (line2 >= text_area.getFirstLine &&
             line1 <= text_area.getFirstLine + text_area.getVisibleLines)
           visible_change = true
@@ -152,18 +150,14 @@
     {
       Swing_Thread.now {
         val snapshot = model.snapshot()
-        val document = snapshot.document
-        val doc = snapshot.node
-        def from_current(pos: Int) = model.from_current(document, pos)
-        def to_current(pos: Int) = model.to_current(document, pos)
 
         val command_range: Iterable[(Command, Int)] =
         {
-          val range = doc.command_range(from_current(start(0)))
+          val range = snapshot.node.command_range(snapshot.from_current(start(0)))
           if (range.hasNext) {
             val (cmd0, start0) = range.next
             new Iterable[(Command, Int)] {
-              def iterator = Document.command_starts(doc.commands.iterator(cmd0), start0)
+              def iterator = Document.command_starts(snapshot.node.commands.iterator(cmd0), start0)
             }
           }
           else Iterable.empty
@@ -177,15 +171,17 @@
               val line_start = start(i)
               val line_end = model.visible_line_end(line_start, end(i))
 
-              val a = from_current(line_start)
-              val b = from_current(line_end)
+              val a = snapshot.from_current(line_start)
+              val b = snapshot.from_current(line_end)
               val cmds = command_range.iterator.
                 dropWhile { case (cmd, c) => c + cmd.length <= a } .
                 takeWhile { case (_, c) => c < b }
 
               for ((command, command_start) <- cmds if !command.is_ignored) {
-                val p = text_area.offsetToXY(line_start max to_current(command_start))
-                val q = text_area.offsetToXY(line_end min to_current(command_start + command.length))
+                val p = text_area.offsetToXY(
+                  line_start max snapshot.to_current(command_start))
+                val q = text_area.offsetToXY(
+                  line_end min snapshot.to_current(command_start + command.length))
                 assert(p.y == q.y)
                 gfx.setColor(Document_View.choose_color(snapshot, command))
                 gfx.fillRect(p.x, y, q.x - p.x, line_height)
@@ -201,12 +197,10 @@
     override def getToolTipText(x: Int, y: Int): String =
     {
       val snapshot = model.snapshot()
-      val document = snapshot.document
-      val doc = snapshot.node
-      val offset = model.from_current(document, text_area.xyToOffset(x, y))
-      doc.command_at(offset) match {
+      val offset = snapshot.from_current(text_area.xyToOffset(x, y))
+      snapshot.node.command_at(offset) match {
         case Some((command, command_start)) =>
-          document.current_state(command).type_at(offset - command_start) match {
+          snapshot.document.current_state(command).type_at(offset - command_start) match {
             case Some(text) => Isabelle.tooltip(text)
             case None => null
           }
@@ -270,12 +264,11 @@
       super.paintComponent(gfx)
       val buffer = model.buffer
       val snapshot = model.snapshot()
-      def to_current(pos: Int) = model.to_current(snapshot.document, pos)
       val saved_color = gfx.getColor  // FIXME needed!?
       try {
         for ((command, start) <- snapshot.node.command_starts if !command.is_ignored) {
-          val line1 = buffer.getLineOfOffset(to_current(start))
-          val line2 = buffer.getLineOfOffset(to_current(start + command.length)) + 1
+          val line1 = buffer.getLineOfOffset(snapshot.to_current(start))
+          val line2 = buffer.getLineOfOffset(snapshot.to_current(start + command.length)) + 1
           val y = line_to_y(line1)
           val height = HEIGHT * (line2 - line1)
           gfx.setColor(Document_View.choose_color(snapshot, command))
diff -r 2837c952ca31 -r eab0d1c2e46e src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Thu Aug 05 16:58:18 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Thu Aug 05 18:00:37 2010 +0200
@@ -43,26 +43,24 @@
     Document_Model(buffer) match {
       case Some(model) =>
         val snapshot = model.snapshot()
-        val document = snapshot.document
-        val doc = snapshot.node
-        val offset = model.from_current(document, original_offset)
-        doc.command_at(offset) match {
+        val offset = snapshot.from_current(original_offset)
+        snapshot.node.command_at(offset) match {
           case Some((command, command_start)) =>
-            document.current_state(command).ref_at(offset - command_start) match {
+            snapshot.document.current_state(command).ref_at(offset - command_start) match {
               case Some(ref) =>
-                val begin = model.to_current(document, command_start + ref.start)
+                val begin = snapshot.to_current(command_start + ref.start)
                 val line = buffer.getLineOfOffset(begin)
-                val end = model.to_current(document, command_start + ref.stop)
+                val end = snapshot.to_current(command_start + ref.stop)
                 ref.info match {
                   case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) =>
                     new External_Hyperlink(begin, end, line, ref_file, ref_line)
                   case Command.RefInfo(_, _, Some(id), Some(offset)) =>
                     Isabelle.session.lookup_entity(id) match {
                       case Some(ref_cmd: Command) =>
-                        doc.command_start(ref_cmd) match {
+                        snapshot.node.command_start(ref_cmd) match {
                           case Some(ref_cmd_start) =>
                             new Internal_Hyperlink(begin, end, line,
-                              model.to_current(document, ref_cmd_start + offset - 1))
+                              snapshot.to_current(ref_cmd_start + offset - 1))
                           case None => null // FIXME external ref
                         }
                       case _ => null
diff -r 2837c952ca31 -r eab0d1c2e46e src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Thu Aug 05 16:58:18 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Thu Aug 05 18:00:37 2010 +0200
@@ -128,11 +128,9 @@
     import Isabelle_Sidekick.int_to_pos
 
     val root = data.root
-    val snapshot = model.snapshot()
-    val document = snapshot.document
-    val doc = snapshot.node  // FIXME cover all nodes (!??)
-    for ((command, command_start) <- doc.command_range(0) if !stopped) {
-      root.add(document.current_state(command).markup_root.swing_tree((node: Markup_Node) =>
+    val snapshot = model.snapshot()  // FIXME cover all nodes (!??)
+    for ((command, command_start) <- snapshot.node.command_range(0) if !stopped) {
+      root.add(snapshot.document.current_state(command).markup_root.swing_tree((node: Markup_Node) =>
           {
             val content = command.source(node.start, node.stop).replace('\n', ' ')
             val id = command.id
diff -r 2837c952ca31 -r eab0d1c2e46e src/Tools/jEdit/src/jedit/isabelle_token_marker.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Thu Aug 05 16:58:18 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Thu Aug 05 18:00:37 2010 +0200
@@ -152,10 +152,6 @@
     val stop = start + line_segment.count
 
     val snapshot = model.snapshot()
-    val document = snapshot.document
-    val doc = snapshot.node
-    def to: Int => Int = model.to_current(document, _)
-    def from: Int => Int = model.from_current(document, _)
 
     /* FIXME
     for (text_area <- Isabelle.jedit_text_areas(model.buffer)
@@ -168,10 +164,11 @@
 
     var next_x = start
     for {
-      (command, command_start) <- doc.command_range(from(start), from(stop))
-      markup <- document.current_state(command).highlight.flatten
-      val abs_start = to(command_start + markup.start)
-      val abs_stop = to(command_start + markup.stop)
+      (command, command_start) <-
+        snapshot.node.command_range(snapshot.from_current(start), snapshot.from_current(stop))
+      markup <- snapshot.document.current_state(command).highlight.flatten
+      val abs_start = snapshot.to_current(command_start + markup.start)
+      val abs_stop = snapshot.to_current(command_start + markup.stop)
       if (abs_stop > start)
       if (abs_start < stop)
       val token_start = (abs_start - start) max 0
diff -r 2837c952ca31 -r eab0d1c2e46e src/Tools/jEdit/src/jedit/output_dockable.scala
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Thu Aug 05 16:58:18 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Thu Aug 05 18:00:37 2010 +0200
@@ -65,9 +65,9 @@
         case Some(doc_view) =>
           current_command match {
             case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) =>
-              val document = doc_view.model.snapshot().document
+              val snapshot = doc_view.model.snapshot()
               val filtered_results =
-                document.current_state(cmd).results filter {
+                snapshot.document.current_state(cmd).results filter {
                   case XML.Elem(Markup.TRACING, _, _) => show_tracing
                   case XML.Elem(Markup.DEBUG, _, _) => show_debug
                   case _ => true