# HG changeset patch
# User wenzelm
# Date 1376320287 -7200
# Node ID 28f59ca8ce781552e35bde4ee5f687be592b4275
# Parent  575be709c83ef6bffc03aed9f3480ef2d44f3ccb
manage hyperlinks via PIDE editor interface;

diff -r 575be709c83e -r 28f59ca8ce78 src/Pure/PIDE/editor.scala
--- a/src/Pure/PIDE/editor.scala	Mon Aug 12 15:09:13 2013 +0200
+++ b/src/Pure/PIDE/editor.scala	Mon Aug 12 17:11:27 2013 +0200
@@ -20,5 +20,10 @@
   def node_overlays(name: Document.Node.Name): Document.Node.Overlays
   def insert_overlay(command: Command, fn: String, args: List[String]): Unit
   def remove_overlay(command: Command, fn: String, args: List[String]): Unit
+
+  abstract class Hyperlink { def follow(context: Context): Unit }
+  def hyperlink_file(file_name: String, line: Int = 0, column: Int = 0): Hyperlink
+  def hyperlink_command(
+    snapshot: Document.Snapshot, command: Command, offset: Text.Offset = 0): Option[Hyperlink]
 }
 
diff -r 575be709c83e -r 28f59ca8ce78 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Mon Aug 12 15:09:13 2013 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Mon Aug 12 17:11:27 2013 +0200
@@ -17,7 +17,6 @@
   "src/fold_handling.scala"
   "src/graphview_dockable.scala"
   "src/html_panel.scala"
-  "src/hyperlink.scala"
   "src/info_dockable.scala"
   "src/isabelle.scala"
   "src/isabelle_encoding.scala"
diff -r 575be709c83e -r 28f59ca8ce78 src/Tools/jEdit/src/documentation_dockable.scala
--- a/src/Tools/jEdit/src/documentation_dockable.scala	Mon Aug 12 15:09:13 2013 +0200
+++ b/src/Tools/jEdit/src/documentation_dockable.scala	Mon Aug 12 17:11:27 2013 +0200
@@ -66,7 +66,7 @@
                         "Documentation error", GUI.scrollable_text(Exn.message(exn)))
                   })
               case Text_File(_, path) =>
-                Hyperlink(Isabelle_System.platform_path(path)).follow(view)
+                PIDE.editor.goto(view, Isabelle_System.platform_path(path))
               case _ =>
             }
           case _ =>
diff -r 575be709c83e -r 28f59ca8ce78 src/Tools/jEdit/src/hyperlink.scala
--- a/src/Tools/jEdit/src/hyperlink.scala	Mon Aug 12 15:09:13 2013 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,58 +0,0 @@
-/*  Title:      Tools/jEdit/src/hyperlink.scala
-    Author:     Fabian Immler, TU Munich
-    Author:     Makarius
-
-Hyperlinks within jEdit buffers for PIDE proof documents.
-*/
-
-package isabelle.jedit
-
-
-import isabelle._
-
-import org.gjt.sp.jedit.{View, jEdit}
-import org.gjt.sp.jedit.textarea.JEditTextArea
-
-
-object Hyperlink
-{
-  def apply(jedit_file: String, line: Int = 0, column: Int = 0): Hyperlink =
-    File_Link(jedit_file, line, column)
-}
-
-abstract class Hyperlink
-{
-  def follow(view: View): Unit
-}
-
-private case class File_Link(jedit_file: String, line: Int, column: Int) extends Hyperlink
-{
-  override def follow(view: View)
-  {
-    Swing_Thread.require()
-
-    JEdit_Lib.jedit_buffer(jedit_file) match {
-      case Some(buffer) =>
-        view.goToBuffer(buffer)
-        val text_area = view.getTextArea
-
-        try {
-          val line_start = text_area.getBuffer.getLineStartOffset(line - 1)
-          text_area.moveCaretPosition(line_start)
-          if (column > 0) text_area.moveCaretPosition(line_start + column - 1)
-        }
-        catch {
-          case _: ArrayIndexOutOfBoundsException =>
-          case _: IllegalArgumentException =>
-        }
-
-      case None =>
-        val args =
-          if (line <= 0) Array(jedit_file)
-          else if (column <= 0) Array(jedit_file, "+line:" + line.toInt)
-          else Array(jedit_file, "+line:" + line.toInt + "," + column.toInt)
-        jEdit.openFiles(view, null, args)
-    }
-  }
-}
-
diff -r 575be709c83e -r 28f59ca8ce78 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Aug 12 15:09:13 2013 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Aug 12 17:11:27 2013 +0200
@@ -17,9 +17,9 @@
 {
   /* session */
 
-  def session: Session = PIDE.session
+  override def session: Session = PIDE.session
 
-  def flush()
+  override def flush()
   {
     Swing_Thread.require()
 
@@ -39,16 +39,16 @@
 
   /* current situation */
 
-  def current_context: View =
+  override def current_context: View =
     Swing_Thread.require { jEdit.getActiveView() }
 
-  def current_node(view: View): Option[Document.Node.Name] =
+  override def current_node(view: View): Option[Document.Node.Name] =
     Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.node_name) }
 
-  def current_node_snapshot(view: View): Option[Document.Snapshot] =
+  override def current_node_snapshot(view: View): Option[Document.Snapshot] =
     Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.snapshot()) }
 
-  def node_snapshot(name: Document.Node.Name): Document.Snapshot =
+  override def node_snapshot(name: Document.Node.Name): Document.Snapshot =
   {
     Swing_Thread.require()
 
@@ -62,7 +62,8 @@
     }
   }
 
-  def current_command(view: View, snapshot: Document.Snapshot): Option[(Command, Text.Offset)] =
+  override def current_command(view: View, snapshot: Document.Snapshot)
+    : Option[(Command, Text.Offset)] =
   {
     Swing_Thread.require()
 
@@ -84,12 +85,65 @@
 
   private var overlays = Document.Overlays.empty
 
-  def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
+  override def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
     synchronized { overlays(name) }
 
-  def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
+  override def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
     synchronized { overlays = overlays.insert(command, fn, args) }
 
-  def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
+  override def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
     synchronized { overlays = overlays.remove(command, fn, args) }
+
+
+  /* hyperlinks */
+
+  def goto(view: View, file_name: String, line: Int = 0, column: Int = 0)
+  {
+    Swing_Thread.require()
+
+    JEdit_Lib.jedit_buffer(file_name) match {
+      case Some(buffer) =>
+        view.goToBuffer(buffer)
+        val text_area = view.getTextArea
+
+        try {
+          val line_start = text_area.getBuffer.getLineStartOffset(line - 1)
+          text_area.moveCaretPosition(line_start)
+          if (column > 0) text_area.moveCaretPosition(line_start + column - 1)
+        }
+        catch {
+          case _: ArrayIndexOutOfBoundsException =>
+          case _: IllegalArgumentException =>
+        }
+
+      case None =>
+        val args =
+          if (line <= 0) Array(file_name)
+          else if (column <= 0) Array(file_name, "+line:" + line.toInt)
+          else Array(file_name, "+line:" + line.toInt + "," + column.toInt)
+        jEdit.openFiles(view, null, args)
+    }
+  }
+
+  override def hyperlink_file(file_name: String, line: Int = 0, column: Int = 0): Hyperlink =
+    new Hyperlink { def follow(view: View) = goto(view, file_name, line, column) }
+
+  override def hyperlink_command(snapshot: Document.Snapshot, command: Command, offset: Int = 0)
+    : Option[Hyperlink] =
+  {
+    if (snapshot.is_outdated) None
+    else {
+      snapshot.state.find_command(snapshot.version, command.id) match {
+        case None => None
+        case Some((node, _)) =>
+          val file_name = command.node_name.node
+          val sources =
+            node.commands.iterator.takeWhile(_ != command).map(_.source) ++
+              (if (offset == 0) Iterator.empty
+               else Iterator.single(command.source(Text.Range(0, command.decode(offset)))))
+          val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
+          Some(new Hyperlink { def follow(view: View) { goto(view, file_name, line, column) } })
+      }
+    }
+  }
 }
diff -r 575be709c83e -r 28f59ca8ce78 src/Tools/jEdit/src/query_operation.scala
--- a/src/Tools/jEdit/src/query_operation.scala	Mon Aug 12 15:09:13 2013 +0200
+++ b/src/Tools/jEdit/src/query_operation.scala	Mon Aug 12 17:11:27 2013 +0200
@@ -12,8 +12,6 @@
 
 import scala.actors.Actor._
 
-import org.gjt.sp.jedit.View
-
 
 object Query_Operation
 {
@@ -25,9 +23,9 @@
   }
 }
 
-class Query_Operation(
-  editor: Editor[View],
-  view: View,
+class Query_Operation[Editor_Context](
+  editor: Editor[Editor_Context],
+  editor_context: Editor_Context,
   operation_name: String,
   consume_status: Query_Operation.Status.Value => Unit,
   consume_output: (Document.Snapshot, Command.Results, XML.Body) => Unit)
@@ -151,12 +149,12 @@
   {
     Swing_Thread.require()
 
-    editor.current_node_snapshot(view) match {
+    editor.current_node_snapshot(editor_context) match {
       case Some(snapshot) =>
         remove_overlay()
         reset_state()
         consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
-        editor.current_command(view, snapshot) match {
+        editor.current_command(editor_context, snapshot) match {
           case Some((command, _)) =>
             current_location = Some(command)
             current_query = query
@@ -174,18 +172,11 @@
   {
     Swing_Thread.require()
 
-    current_location match {
-      case Some(command) =>
-        val snapshot = editor.node_snapshot(command.node_name)
-        val commands = snapshot.node.commands
-        if (commands.contains(command)) {
-          // FIXME revert offset (!?)
-          val sources = commands.iterator.takeWhile(_ != command).map(_.source)
-          val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
-          Hyperlink(command.node_name.node, line, column).follow(view)
-        }
-      case None =>
-    }
+    for {
+      command <- current_location
+      snapshot = editor.node_snapshot(command.node_name)
+      link <- editor.hyperlink_command(snapshot, command)
+    } link.follow(editor_context)
   }
 
 
diff -r 575be709c83e -r 28f59ca8ce78 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Mon Aug 12 15:09:13 2013 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Mon Aug 12 17:11:27 2013 +0200
@@ -199,15 +199,16 @@
 
   private val hyperlink_include = Set(Markup.ENTITY, Markup.PATH)
 
-  def hyperlink(range: Text.Range): Option[Text.Info[Hyperlink]] =
+  def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
   {
-    snapshot.cumulate_markup[List[Text.Info[Hyperlink]]](range, Nil, Some(hyperlink_include), _ =>
+    snapshot.cumulate_markup[List[Text.Info[PIDE.editor.Hyperlink]]](
+      range, Nil, Some(hyperlink_include), _ =>
         {
           case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
           if Path.is_ok(name) =>
             val jedit_file = PIDE.thy_load.append(snapshot.node_name.dir, Path.explode(name))
-            val link = Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, 0, 0))
-            Some(link :: links)
+            val link = PIDE.editor.hyperlink_file(jedit_file)
+            Some(Text.Info(snapshot.convert(info_range), link) :: links)
 
           case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _)))
           if !props.exists(
@@ -220,23 +221,16 @@
                 Isabelle_System.source_file(Path.explode(name)) match {
                   case Some(path) =>
                     val jedit_file = Isabelle_System.platform_path(path)
-                    val link =
-                      Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, line, 0))
-                    Some(link :: links)
+                    val link = PIDE.editor.hyperlink_file(jedit_file, line)
+                    Some(Text.Info(snapshot.convert(info_range), link) :: links)
                   case None => None
                 }
 
               case Position.Def_Id_Offset(id, offset) =>
                 snapshot.state.find_command(snapshot.version, id) match {
                   case Some((node, command)) =>
-                    val sources =
-                      node.commands.iterator.takeWhile(_ != command).map(_.source) ++
-                        Iterator.single(command.source(Text.Range(0, command.decode(offset))))
-                    val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
-                    val link =
-                      Text.Info(snapshot.convert(info_range),
-                        Hyperlink(command.node_name.node, line, column))
-                    Some(link :: links)
+                    PIDE.editor.hyperlink_command(snapshot, command, offset)
+                      .map(link => (Text.Info(snapshot.convert(info_range), link) :: links))
                   case None => None
                 }
 
diff -r 575be709c83e -r 28f59ca8ce78 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Mon Aug 12 15:09:13 2013 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Mon Aug 12 17:11:27 2013 +0200
@@ -135,7 +135,8 @@
   private var control: Boolean = false
 
   private val highlight_area = new Active_Area[Color]((r: Rendering) => r.highlight _)
-  private val hyperlink_area = new Active_Area[Hyperlink]((r: Rendering) => r.hyperlink _)
+  private val hyperlink_area =
+    new Active_Area[PIDE.editor.Hyperlink]((r: Rendering) => r.hyperlink _)
   private val active_area = new Active_Area[XML.Elem]((r: Rendering) => r.active _)
 
   private val active_areas =
diff -r 575be709c83e -r 28f59ca8ce78 src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Mon Aug 12 15:09:13 2013 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Mon Aug 12 17:11:27 2013 +0200
@@ -41,7 +41,7 @@
               } model.node_required = !model.node_required
             }
           }
-          else if (clicks == 2) Hyperlink(listData(index).node).follow(view)
+          else if (clicks == 2) PIDE.editor.goto(view, listData(index).node)
         }
       case MouseMoved(_, point, _) =>
         val index = peer.locationToIndex(point)
diff -r 575be709c83e -r 28f59ca8ce78 src/Tools/jEdit/src/timing_dockable.scala
--- a/src/Tools/jEdit/src/timing_dockable.scala	Mon Aug 12 15:09:13 2013 +0200
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Mon Aug 12 17:11:27 2013 +0200
@@ -89,22 +89,14 @@
     extends Entry
   {
     def print: String = Time.print_seconds(timing) + "s theory " + quote(name.theory)
-    def follow(snapshot: Document.Snapshot): Unit = Hyperlink(name.node).follow(view)
+    def follow(snapshot: Document.Snapshot) { PIDE.editor.goto(view, name.node) }
   }
 
   private case class Command_Entry(command: Command, timing: Double) extends Entry
   {
     def print: String = "  " + Time.print_seconds(timing) + "s command " + quote(command.name)
-
     def follow(snapshot: Document.Snapshot)
-    {
-      val node = snapshot.version.nodes(command.node_name)
-      if (node.commands.contains(command)) {
-        val sources = node.commands.iterator.takeWhile(_ != command).map(_.source)
-        val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
-        Hyperlink(command.node_name.node, line, column).follow(view)
-      }
-    }
+    { PIDE.editor.hyperlink_command(snapshot, command).foreach(_.follow(view)) }
   }