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) } })
+      }
+    }
+  }
 }