# HG changeset patch
# User wenzelm
# Date 1314711807 -7200
# Node ID 3bc9a215a56d3efce497f245722d63cc02963b03
# Parent  a9cf2380377da3387b13087ee75aed16a221eaff
some support for hyperlinks between different buffers;
tuned signature;

diff -r a9cf2380377d -r 3bc9a215a56d src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Tue Aug 30 12:24:55 2011 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Aug 30 15:43:27 2011 +0200
@@ -194,7 +194,7 @@
     val version: Version
     val node: Node
     val is_outdated: Boolean
-    def lookup_command(id: Command_ID): Option[Command]
+    def find_command(id: Command_ID): Option[(String, Node, Command)]
     def state(command: Command): Command.State
     def convert(i: Text.Offset): Text.Offset
     def convert(range: Text.Range): Text.Range
@@ -370,7 +370,13 @@
         val node = version.nodes(name)
         val is_outdated = !(pending_edits.isEmpty && latest == stable)
 
-        def lookup_command(id: Command_ID): Option[Command] = State.this.lookup_command(id)
+        def find_command(id: Command_ID): Option[(String, Node, Command)] =
+          State.this.lookup_command(id) match {
+            case None => None
+            case Some(command) =>
+              version.nodes.find({ case (_, node) => node.commands(command) })
+                .map({ case (name, node) => (name, node, command) })
+          }
 
         def state(command: Command): Command.State =
           try {
diff -r a9cf2380377d -r 3bc9a215a56d src/Tools/jEdit/src/isabelle_hyperlinks.scala
--- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Tue Aug 30 12:24:55 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Tue Aug 30 15:43:27 2011 +0200
@@ -16,11 +16,21 @@
 import org.gjt.sp.jedit.{View, jEdit, Buffer, TextUtilities}
 
 
-private class Internal_Hyperlink(start: Int, end: Int, line: Int, def_offset: Int)
+private class Internal_Hyperlink(name: String, start: Int, end: Int, line: Int, offset: Int)
   extends AbstractHyperlink(start, end, line, "")
 {
-  override def click(view: View) {
-    view.getTextArea.moveCaretPosition(def_offset)
+  override def click(view: View)
+  {
+    val text_area = view.getTextArea
+    if (Isabelle.buffer_name(view.getBuffer) == name)
+      text_area.moveCaretPosition(offset)
+    else
+      Isabelle.jedit_buffer(name) match {
+        case Some(buffer) =>
+          view.setBuffer(buffer)
+          text_area.moveCaretPosition(offset)
+        case None =>
+      }
   }
 }
 
@@ -60,21 +70,22 @@
                 (Position.File.unapply(props), Position.Line.unapply(props)) match {
                   case (Some(def_file), Some(def_line)) =>
                     new External_Hyperlink(begin, end, line, def_file, def_line)
-                  case _ =>
+                  case _ if !snapshot.is_outdated =>
                     (props, props) match {
                       case (Position.Id(def_id), Position.Offset(def_offset)) =>
-                        snapshot.lookup_command(def_id) match {
-                          case Some(def_cmd) =>
-                            snapshot.node.command_start(def_cmd) match {
+                        snapshot.find_command(def_id) match {
+                          case Some((def_name, def_node, def_cmd)) =>
+                            def_node.command_start(def_cmd) match {
                               case Some(def_cmd_start) =>
-                                new Internal_Hyperlink(begin, end, line,
-                                  snapshot.convert(def_cmd_start + def_cmd.decode(def_offset)))
+                                new Internal_Hyperlink(def_name, begin, end, line,
+                                  def_cmd_start + def_cmd.decode(def_offset))
                               case None => null
                             }
                           case None => null
                         }
                       case _ => null
                     }
+                  case _ => null
                 }
             }
           markup match {
diff -r a9cf2380377d -r 3bc9a215a56d src/Tools/jEdit/src/jedit_thy_load.scala
--- a/src/Tools/jEdit/src/jedit_thy_load.scala	Tue Aug 30 12:24:55 2011 +0200
+++ b/src/Tools/jEdit/src/jedit_thy_load.scala	Tue Aug 30 15:43:27 2011 +0200
@@ -49,7 +49,7 @@
   override def check_thy(node_name: String): Thy_Header =
   {
     Swing_Thread.now {
-      Isabelle.jedit_buffers().find(buffer => Isabelle.buffer_name(buffer) == node_name) match {
+      Isabelle.jedit_buffer(node_name) match {
         case Some(buffer) =>
           Isabelle.buffer_lock(buffer) {
             val text = new Segment
diff -r a9cf2380377d -r 3bc9a215a56d src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Tue Aug 30 12:24:55 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Tue Aug 30 15:43:27 2011 +0200
@@ -159,10 +159,27 @@
   }
 
 
+  /* buffers */
+
+  def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
+    Swing_Thread.now { buffer_lock(buffer) { body } }
+
+  def buffer_text(buffer: JEditBuffer): String =
+    buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
+
+  def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
+
+  def buffer_path(buffer: Buffer): (String, String) =
+    (buffer.getDirectory, buffer_name(buffer))
+
+
   /* main jEdit components */
 
   def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
 
+  def jedit_buffer(name: String): Option[Buffer] =
+    jedit_buffers().find(buffer => buffer_name(buffer) == name)
+
   def jedit_views(): Iterator[View] = jEdit.getViews().iterator
 
   def jedit_text_areas(view: View): Iterator[JEditTextArea] =
@@ -180,17 +197,6 @@
     finally { buffer.readUnlock() }
   }
 
-  def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
-    Swing_Thread.now { buffer_lock(buffer) { body } }
-
-  def buffer_text(buffer: JEditBuffer): String =
-    buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
-
-  def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
-
-  def buffer_path(buffer: Buffer): (String, String) =
-    (buffer.getDirectory, buffer_name(buffer))
-
 
   /* document model and view */