--- 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]
}
--- 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"
--- 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 _ =>
--- 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)
- }
- }
-}
-
--- 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) } })
+ }
+ }
+ }
}
--- 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)
}
--- 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
}
--- 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 =
--- 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)
--- 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)) }
}