# HG changeset patch
# User wenzelm
# Date 1347989625 -7200
# Node ID e2726211f834e3e2ca5ed17daecceffe96680e6c
# Parent  c451856129cd98d1493dc3d8b871baebf66b86fd
pass base_snapshot to enable hyperlinks into other nodes;
clarified "def" positions: refrain from renaming properties;
clarified snapshot.is_output vs. output and hyperlinks;

diff -r c451856129cd -r e2726211f834 src/Pure/General/position.scala
--- a/src/Pure/General/position.scala	Tue Sep 18 17:20:40 2012 +0200
+++ b/src/Pure/General/position.scala	Tue Sep 18 19:33:45 2012 +0200
@@ -20,6 +20,12 @@
   val File = new Properties.String(Isabelle_Markup.FILE)
   val Id = new Properties.Long(Isabelle_Markup.ID)
 
+  val Def_Line = new Properties.Int(Isabelle_Markup.DEF_LINE)
+  val Def_Offset = new Properties.Int(Isabelle_Markup.DEF_OFFSET)
+  val Def_End_Offset = new Properties.Int(Isabelle_Markup.DEF_END_OFFSET)
+  val Def_File = new Properties.String(Isabelle_Markup.DEF_FILE)
+  val Def_Id = new Properties.Long(Isabelle_Markup.DEF_ID)
+
   object Line_File
   {
     def unapply(pos: T): Option[(Int, String)] =
@@ -30,6 +36,16 @@
       }
   }
 
+  object Def_Line_File
+  {
+    def unapply(pos: T): Option[(Int, String)] =
+      (pos, pos) match {
+        case (Def_Line(i), Def_File(name)) => Some((i, name))
+        case (_, Def_File(name)) => Some((1, name))
+        case _ => None
+      }
+  }
+
   object Range
   {
     def apply(range: Text.Range): T = Offset(range.start) ++ Offset(range.stop)
@@ -50,6 +66,15 @@
       }
   }
 
+  object Def_Id_Offset
+  {
+    def unapply(pos: T): Option[(Long, Text.Offset)] =
+      (pos, pos) match {
+        case (Def_Id(id), Def_Offset(offset)) => Some((id, offset))
+        case _ => None
+      }
+  }
+
   object Id_Range
   {
     def unapply(pos: T): Option[(Long, Text.Range)] =
@@ -59,16 +84,7 @@
       }
   }
 
-  private val purge_pos = Map(
-    Isabelle_Markup.DEF_LINE -> Isabelle_Markup.LINE,
-    Isabelle_Markup.DEF_OFFSET -> Isabelle_Markup.OFFSET,
-    Isabelle_Markup.DEF_END_OFFSET -> Isabelle_Markup.END_OFFSET,
-    Isabelle_Markup.DEF_FILE -> Isabelle_Markup.FILE,
-    Isabelle_Markup.DEF_ID -> Isabelle_Markup.ID)
-
-  def purge(props: T): T =
-    for ((x, y) <- props if !Isabelle_Markup.POSITION_PROPERTIES(x))
-      yield (if (purge_pos.isDefinedAt(x)) (purge_pos(x), y) else (x, y))
+  def purge(props: T): T = props.filterNot(p => Isabelle_Markup.POSITION_PROPERTIES(p._1))
 
 
   /* here: inlined formal markup */
diff -r c451856129cd -r e2726211f834 src/Tools/jEdit/src/isabelle_rendering.scala
--- a/src/Tools/jEdit/src/isabelle_rendering.scala	Tue Sep 18 17:20:40 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Tue Sep 18 19:33:45 2012 +0200
@@ -206,7 +206,7 @@
               case _ => false }).isEmpty) =>
 
             props match {
-              case Position.Line_File(line, name) if Path.is_ok(name) =>
+              case Position.Def_Line_File(line, name) if Path.is_ok(name) =>
                 Isabelle_System.source_file(Path.explode(name)) match {
                   case Some(path) =>
                     val jedit_file = Isabelle_System.platform_path(path)
@@ -214,7 +214,7 @@
                   case None => links
                 }
 
-              case Position.Id_Offset(id, offset) if !snapshot.is_outdated =>
+              case Position.Def_Id_Offset(id, offset) =>
                 snapshot.state.find_command(snapshot.version, id) match {
                   case Some((node, command)) =>
                     val sources =
diff -r c451856129cd -r e2726211f834 src/Tools/jEdit/src/output2_dockable.scala
--- a/src/Tools/jEdit/src/output2_dockable.scala	Tue Sep 18 17:20:40 2012 +0200
+++ b/src/Tools/jEdit/src/output2_dockable.scala	Tue Sep 18 19:33:45 2012 +0200
@@ -31,6 +31,7 @@
   private var zoom_factor = 100
   private var show_tracing = false
   private var do_update = true
+  private var current_snapshot = Document.State.init.snapshot()
   private var current_state = Command.empty.init_state
   private var current_output: List[XML.Tree] = Nil
 
@@ -53,19 +54,21 @@
   {
     Swing_Thread.require()
 
-    val new_state =
-      if (follow) {
-        Document_View(view.getTextArea) match {
-          case Some(doc_view) =>
-            val snapshot = doc_view.model.snapshot()
+    val (new_snapshot, new_state) =
+      Document_View(view.getTextArea) match {
+        case Some(doc_view) =>
+          val snapshot = doc_view.model.snapshot()
+          if (follow && !snapshot.is_outdated) {
             snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match {
-              case Some(cmd) => snapshot.state.command_state(snapshot.version, cmd)
-              case None => Command.empty.init_state
+              case Some(cmd) =>
+                (snapshot, snapshot.state.command_state(snapshot.version, cmd))
+              case None =>
+                (Document.State.init.snapshot(), Command.empty.init_state)
             }
-          case None => Command.empty.init_state
-        }
+          }
+          else (current_snapshot, current_state)
+        case None => (current_snapshot, current_state)
       }
-      else current_state
 
     val new_output =
       if (!restriction.isDefined || restriction.get.contains(new_state.command))
@@ -74,8 +77,9 @@
       else current_output
 
     if (new_output != current_output)
-      pretty_text_area.update(Library.separate(Pretty.FBreak, new_output))
+      pretty_text_area.update(new_snapshot, Library.separate(Pretty.FBreak, new_output))
 
+    current_snapshot = new_snapshot
     current_state = new_state
     current_output = new_output
   }
diff -r c451856129cd -r e2726211f834 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Tue Sep 18 17:20:40 2012 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Tue Sep 18 19:33:45 2012 +0200
@@ -20,18 +20,20 @@
 
 object Pretty_Text_Area
 {
-  def document_state(formatted_body: XML.Body): (String, Document.State) =
+  def document_state(base_snapshot: Document.Snapshot, formatted_body: XML.Body)
+    : (String, Document.State) =
   {
     val command = Command.rich_text(Document.new_id(), formatted_body)
     val node_name = command.node_name
-
     val edits: List[Document.Edit_Text] =
       List(node_name -> Document.Node.Edits(List(Text.Edit.insert(0, command.source))))
 
-    val state0 = Document.State.init.define_command(command)
-    val version0 = state0.history.tip.version.get_finished
+    val state0 = base_snapshot.state.define_command(command)
+    val version0 = base_snapshot.version
     val nodes0 = version0.nodes
 
+    assert(nodes0(node_name).commands.isEmpty)
+
     val nodes1 = nodes0 + (node_name -> nodes0(node_name).update_commands(Linear_Set(command)))
     val version1 = Document.Version.make(version0.syntax, nodes1)
     val state1 =
@@ -52,6 +54,7 @@
   private var current_font_size: Int = 12
   private var current_margin: Int = 0
   private var current_body: XML.Body = Nil
+  private var current_base_snapshot = Document.State.init.snapshot()
   private var current_rendering: Isabelle_Rendering = text_rendering()._2
 
   val text_area = new JEditEmbeddedTextArea
@@ -63,7 +66,7 @@
 
     val body =
       Pretty.formatted(current_body, current_margin, Pretty.font_metric(current_font_metrics))
-    val (text, state) = Pretty_Text_Area.document_state(body)
+    val (text, state) = Pretty_Text_Area.document_state(current_base_snapshot, body)
     val rendering = Isabelle_Rendering(state.snapshot(), Isabelle.options.value)
 
     (text, rendering)
@@ -106,10 +109,12 @@
     refresh()
   }
 
-  def update(body: XML.Body)
+  def update(base_snapshot: Document.Snapshot, body: XML.Body)
   {
     Swing_Thread.require()
+    require(!base_snapshot.is_outdated)
 
+    current_base_snapshot = base_snapshot
     current_body = body
     refresh()
   }