# HG changeset patch
# User wenzelm
# Date 1281020298 -7200
# Node ID 2837c952ca3142a693814d75427702d51c649691
# Parent  67fc24df3721cdf696c3d29a37436bc7027b8bc9
explicit Change.Snapshot and Document.Node;
misc tuning and clarification;
Document_View: explicitly highlight outdated command status;

diff -r 67fc24df3721 -r 2837c952ca31 src/Pure/PIDE/change.scala
--- a/src/Pure/PIDE/change.scala	Thu Aug 05 14:35:35 2010 +0200
+++ b/src/Pure/PIDE/change.scala	Thu Aug 05 16:58:18 2010 +0200
@@ -2,7 +2,7 @@
     Author:     Fabian Immler, TU Munich
     Author:     Makarius
 
-Changes of plain text.
+Changes of plain text, resulting in document edits.
 */
 
 package isabelle
@@ -11,14 +11,25 @@
 object Change
 {
   val init = new Change(Document.NO_ID, None, Nil, Future.value(Nil, Document.init))
+
+  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
+  }
 }
 
 class Change(
   val id: Document.Version_ID,
   val parent: Option[Change],
-  val edits: List[Document.Node.Text_Edit],
+  val edits: List[Document.Node_Text_Edit],
   val result: Future[(List[Document.Edit[Command]], Document)])
 {
+  /* ancestor versions */
+
   def ancestors: Iterator[Change] = new Iterator[Change]
   {
     private var state: Option[Change] = Some(Change.this)
@@ -30,10 +41,10 @@
       }
   }
 
-  def join_document: Document = result.join._2
-  def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished
 
-  def edit(session: Session, edits: List[Document.Node.Text_Edit]): Change =
+  /* editing and state assignment */
+
+  def edit(session: Session, edits: List[Document.Node_Text_Edit]): Change =
   {
     val new_id = session.create_id()
     val result: Future[(List[Document.Edit[Command]], Document)] =
@@ -44,4 +55,21 @@
       }
     new Change(new_id, Some(this), edits, result)
   }
+
+  def join_document: Document = result.join._2
+  def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished
+
+
+  /* snapshot */
+
+  def snapshot(name: String): Change.Snapshot =
+  {
+    val latest = this
+    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)
+    }
+  }
 }
\ No newline at end of file
diff -r 67fc24df3721 -r 2837c952ca31 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Thu Aug 05 14:35:35 2010 +0200
+++ b/src/Pure/PIDE/document.scala	Thu Aug 05 16:58:18 2010 +0200
@@ -23,15 +23,6 @@
   val NO_ID = ""
 
 
-  /* nodes */
-
-  object Node { type Text_Edit = (String, List[isabelle.Text_Edit]) }  // FIXME None: remove
-
-  type Edit[C] =
-   (String,  // node name
-    Option[List[(Option[C], Option[C])]])  // None: remove, Some: insert/remove commands
-
-
   /* command start positions */
 
   def command_starts(commands: Iterator[Command], offset: Int = 0): Iterator[(Command, Int)] =
@@ -45,21 +36,65 @@
   }
 
 
+  /* named document nodes */
+
+  object Node
+  {
+    val empty: Node = new Node(Linear_Set())
+  }
+
+  class Node(val commands: Linear_Set[Command])
+  {
+    /* command ranges */
+
+    def command_starts: Iterator[(Command, Int)] =
+      Document.command_starts(commands.iterator)
+
+    def command_start(cmd: Command): Option[Int] =
+      command_starts.find(_._1 == cmd).map(_._2)
+
+    def command_range(i: Int): Iterator[(Command, Int)] =
+      command_starts dropWhile { case (cmd, start) => start + cmd.length <= i }
+
+    def command_range(i: Int, j: Int): Iterator[(Command, Int)] =
+      command_range(i) takeWhile { case (_, start) => start < j }
+
+    def command_at(i: Int): Option[(Command, Int)] =
+    {
+      val range = command_range(i)
+      if (range.hasNext) Some(range.next) else None
+    }
+
+    def proper_command_at(i: Int): Option[Command] =
+      command_at(i) match {
+        case Some((command, _)) =>
+          commands.reverse_iterator(command).find(cmd => !cmd.is_ignored)
+        case None => None
+      }
+  }
+
+
   /* initial document */
 
   val init: Document =
   {
-    val doc = new Document(NO_ID, Map().withDefaultValue(Linear_Set()), Map())
+    val doc = new Document(NO_ID, Map().withDefaultValue(Node.empty), Map())
     doc.assign_states(Nil)
     doc
   }
 
 
 
-  /** document edits **/
+  /** editing **/
+
+  type Node_Text_Edit = (String, List[Text_Edit])  // FIXME None: remove
+
+  type Edit[C] =
+   (String,  // node name
+    Option[List[(Option[C], Option[C])]])  // None: remove, Some: insert/remove commands
 
   def text_edits(session: Session, old_doc: Document, new_id: Version_ID,
-      edits: List[Node.Text_Edit]): (List[Edit[Command]], Document) =
+      edits: List[Node_Text_Edit]): (List[Edit[Command]], Document) =
   {
     require(old_doc.assignment.is_finished)
 
@@ -145,7 +180,7 @@
       var former_states = old_doc.assignment.join
 
       for ((name, text_edits) <- edits) {
-        val commands0 = nodes(name)
+        val commands0 = nodes(name).commands
         val commands1 = edit_text(text_edits, commands0)
         val commands2 = parse_spans(commands1)
 
@@ -157,7 +192,7 @@
           inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
 
         doc_edits += (name -> Some(cmd_edits))
-        nodes += (name -> commands2)
+        nodes += (name -> new Node(commands2))
         former_states --= removed_commands
       }
       (doc_edits.toList, new Document(new_id, nodes, former_states))
@@ -168,39 +203,9 @@
 
 class Document(
     val id: Document.Version_ID,
-    val nodes: Map[String, Linear_Set[Command]],
+    val nodes: Map[String, Document.Node],
     former_states: Map[Command, Command])  // FIXME !?
 {
-  /* command ranges */
-
-  def commands(name: String): Linear_Set[Command] = nodes.get(name) getOrElse Linear_Set()
-
-  def command_starts(name: String): Iterator[(Command, Int)] =
-    Document.command_starts(commands(name).iterator)
-
-  def command_start(name: String, cmd: Command): Option[Int] =
-    command_starts(name).find(_._1 == cmd).map(_._2)
-
-  def command_range(name: String, i: Int): Iterator[(Command, Int)] =
-    command_starts(name) dropWhile { case (cmd, start) => start + cmd.length <= i }
-
-  def command_range(name: String, i: Int, j: Int): Iterator[(Command, Int)] =
-    command_range(name, i) takeWhile { case (_, start) => start < j }
-
-  def command_at(name: String, i: Int): Option[(Command, Int)] =
-  {
-    val range = command_range(name, i)
-    if (range.hasNext) Some(range.next) else None
-  }
-
-  def proper_command_at(name: String, i: Int): Option[Command] =
-    command_at(name, i) match {
-      case Some((command, _)) =>
-        commands(name).reverse_iterator(command).find(cmd => !cmd.is_ignored)
-      case None => None
-    }
-
-
   /* command state assignment */
 
   val assignment = Future.promise[Map[Command, Command]]
diff -r 67fc24df3721 -r 2837c952ca31 src/Tools/jEdit/src/jedit/document_model.scala
--- a/src/Tools/jEdit/src/jedit/document_model.scala	Thu Aug 05 14:35:35 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Thu Aug 05 16:58:18 2010 +0200
@@ -54,6 +54,7 @@
   }
 }
 
+
 class Document_Model(val session: Session, val buffer: Buffer)
 {
   /* visible line end */
@@ -77,7 +78,7 @@
   @volatile private var history = Change.init // owned by Swing thread
 
   def current_change(): Change = history
-  def recent_document(): Document = current_change().ancestors.find(_.is_assigned).get.join_document
+  def snapshot(): Change.Snapshot = current_change().snapshot(thy_name)
 
 
   /* transforming offsets */
diff -r 67fc24df3721 -r 2837c952ca31 src/Tools/jEdit/src/jedit/document_view.scala
--- a/src/Tools/jEdit/src/jedit/document_view.scala	Thu Aug 05 14:35:35 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Thu Aug 05 16:58:18 2010 +0200
@@ -24,10 +24,11 @@
 
 object Document_View
 {
-  def choose_color(document: Document, command: Command): Color =
+  def choose_color(snapshot: Change.Snapshot, command: Command): Color =
   {
-    val state = document.current_state(command)
-    if (state.forks > 0) new Color(255, 228, 225)
+    val state = snapshot.document.current_state(command)
+    if (snapshot.is_outdated) new Color(240, 240, 240)
+    else if (state.forks > 0) new Color(255, 228, 225)
     else if (state.forks < 0) Color.red
     else
       state.status match {
@@ -105,9 +106,9 @@
         case Command_Set(changed) =>
           Swing_Thread.now {
             // FIXME cover doc states as well!!?
-            val document = model.recent_document()
-            if (changed.exists(document.commands(model.thy_name).contains))
-              full_repaint(document, changed)
+            val snapshot = model.snapshot()
+            if (changed.exists(snapshot.node.commands.contains))
+              full_repaint(snapshot, changed)
           }
 
         case bad => System.err.println("command_change_actor: ignoring bad message " + bad)
@@ -115,14 +116,16 @@
     }
   }
 
-  def full_repaint(document: Document, changed: Set[Command])
+  def full_repaint(snapshot: Change.Snapshot, changed: Set[Command])
   {
     Swing_Thread.assert()
 
+    val document = snapshot.document
+    val doc = snapshot.node
     val buffer = model.buffer
     var visible_change = false
 
-    for ((command, start) <- document.command_starts(model.thy_name)) {
+    for ((command, start) <- doc.command_starts) {
       if (changed(command)) {
         val stop = start + command.length
         val line1 = buffer.getLineOfOffset(model.to_current(document, start))
@@ -148,18 +151,19 @@
       start: Array[Int], end: Array[Int], y0: Int, line_height: Int)
     {
       Swing_Thread.now {
-        val document = model.recent_document()
+        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 = document.command_range(model.thy_name, from_current(start(0)))
+          val range = doc.command_range(from_current(start(0)))
           if (range.hasNext) {
             val (cmd0, start0) = range.next
             new Iterable[(Command, Int)] {
-              def iterator =
-                Document.command_starts(document.commands(model.thy_name).iterator(cmd0), start0)
+              def iterator = Document.command_starts(doc.commands.iterator(cmd0), start0)
             }
           }
           else Iterable.empty
@@ -183,7 +187,7 @@
                 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))
                 assert(p.y == q.y)
-                gfx.setColor(Document_View.choose_color(document, command))
+                gfx.setColor(Document_View.choose_color(snapshot, command))
                 gfx.fillRect(p.x, y, q.x - p.x, line_height)
               }
             }
@@ -196,9 +200,11 @@
 
     override def getToolTipText(x: Int, y: Int): String =
     {
-      val document = model.recent_document()
+      val snapshot = model.snapshot()
+      val document = snapshot.document
+      val doc = snapshot.node
       val offset = model.from_current(document, text_area.xyToOffset(x, y))
-      document.command_at(model.thy_name, offset) match {
+      doc.command_at(offset) match {
         case Some((command, command_start)) =>
           document.current_state(command).type_at(offset - command_start) match {
             case Some(text) => Isabelle.tooltip(text)
@@ -213,7 +219,7 @@
   /* caret handling */
 
   def selected_command(): Option[Command] =
-    model.recent_document().proper_command_at(model.thy_name, text_area.getCaretPosition)
+    model.snapshot().node.proper_command_at(text_area.getCaretPosition)
 
   private val caret_listener = new CaretListener {
     private val delay = Swing_Thread.delay_last(session.input_delay) {
@@ -263,16 +269,16 @@
     {
       super.paintComponent(gfx)
       val buffer = model.buffer
-      val document = model.recent_document()
-      def to_current(pos: Int) = model.to_current(document, pos)
+      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) <- document.command_starts(model.thy_name) if !command.is_ignored) {
+        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 y = line_to_y(line1)
           val height = HEIGHT * (line2 - line1)
-          gfx.setColor(Document_View.choose_color(document, command))
+          gfx.setColor(Document_View.choose_color(snapshot, command))
           gfx.fillRect(0, y, getWidth - 1, height)
         }
       }
diff -r 67fc24df3721 -r 2837c952ca31 src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Thu Aug 05 14:35:35 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Thu Aug 05 16:58:18 2010 +0200
@@ -42,9 +42,11 @@
   {
     Document_Model(buffer) match {
       case Some(model) =>
-        val document = model.recent_document()
+        val snapshot = model.snapshot()
+        val document = snapshot.document
+        val doc = snapshot.node
         val offset = model.from_current(document, original_offset)
-        document.command_at(model.thy_name, offset) match {
+        doc.command_at(offset) match {
           case Some((command, command_start)) =>
             document.current_state(command).ref_at(offset - command_start) match {
               case Some(ref) =>
@@ -57,7 +59,7 @@
                   case Command.RefInfo(_, _, Some(id), Some(offset)) =>
                     Isabelle.session.lookup_entity(id) match {
                       case Some(ref_cmd: Command) =>
-                        document.command_start(model.thy_name, ref_cmd) match {
+                        doc.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))
diff -r 67fc24df3721 -r 2837c952ca31 src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Thu Aug 05 14:35:35 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Thu Aug 05 16:58:18 2010 +0200
@@ -95,9 +95,9 @@
     import Isabelle_Sidekick.int_to_pos
 
     val root = data.root
-    val document = model.recent_document()
+    val doc = model.snapshot().node  // FIXME cover all nodes (!??)
     for {
-      (command, command_start) <- document.command_range(model.thy_name, 0)
+      (command, command_start) <- doc.command_range(0)
       if command.is_command && !stopped
     }
     {
@@ -128,8 +128,10 @@
     import Isabelle_Sidekick.int_to_pos
 
     val root = data.root
-    val document = model.recent_document()
-    for ((command, command_start) <- document.command_range(model.thy_name, 0) if !stopped) {
+    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 content = command.source(node.start, node.stop).replace('\n', ' ')
diff -r 67fc24df3721 -r 2837c952ca31 src/Tools/jEdit/src/jedit/isabelle_token_marker.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Thu Aug 05 14:35:35 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Thu Aug 05 16:58:18 2010 +0200
@@ -151,7 +151,9 @@
     val start = model.buffer.getLineStartOffset(line)
     val stop = start + line_segment.count
 
-    val document = model.recent_document()
+    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, _)
 
@@ -166,7 +168,7 @@
 
     var next_x = start
     for {
-      (command, command_start) <- document.command_range(model.thy_name, from(start), from(stop))
+      (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)
diff -r 67fc24df3721 -r 2837c952ca31 src/Tools/jEdit/src/jedit/output_dockable.scala
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Thu Aug 05 14:35:35 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Thu Aug 05 16:58:18 2010 +0200
@@ -65,7 +65,7 @@
         case Some(doc_view) =>
           current_command match {
             case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) =>
-              val document = doc_view.model.recent_document
+              val document = doc_view.model.snapshot().document
               val filtered_results =
                 document.current_state(cmd).results filter {
                   case XML.Elem(Markup.TRACING, _, _) => show_tracing