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