# HG changeset patch # User wenzelm # Date 1393839718 -3600 # Node ID 1421394576536ec9cac2f9bf1af749a17436bd42 # Parent 7f229b0212fe3b581b9b1e05268bc14475f151ce tuned signature; diff -r 7f229b0212fe -r 142139457653 src/Pure/PIDE/editor.scala --- a/src/Pure/PIDE/editor.scala Mon Mar 03 03:13:45 2014 +0100 +++ b/src/Pure/PIDE/editor.scala Mon Mar 03 10:41:58 2014 +0100 @@ -23,9 +23,7 @@ def remove_overlay(command: Command, fn: String, args: List[String]): Unit abstract class Hyperlink { def follow(context: Context): Unit } - def hyperlink_url(name: String): Hyperlink - 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] + snapshot: Document.Snapshot, command: Command, raw_offset: Text.Offset = 0): Option[Hyperlink] } diff -r 7f229b0212fe -r 142139457653 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Mon Mar 03 03:13:45 2014 +0100 +++ b/src/Pure/System/isabelle_system.scala Mon Mar 03 10:41:58 2014 +0100 @@ -212,7 +212,8 @@ if (path.is_absolute || path.is_current) check(path) else { check(Path.explode("~~/src/Pure") + path) orElse - (if (getenv("ML_SOURCES") == "") None else check(Path.explode("$ML_SOURCES") + path)) + (if (getenv("ML_SOURCES") == "") None + else check(Path.explode("$ML_SOURCES") + path)) } } diff -r 7f229b0212fe -r 142139457653 src/Tools/jEdit/src/jedit_editor.scala --- a/src/Tools/jEdit/src/jedit_editor.scala Mon Mar 03 03:13:45 2014 +0100 +++ b/src/Tools/jEdit/src/jedit_editor.scala Mon Mar 03 10:41:58 2014 +0100 @@ -142,20 +142,6 @@ } } - override def hyperlink_url(name: String): Hyperlink = - new Hyperlink { - def follow(view: View) = - default_thread_pool.submit(() => - try { Isabelle_System.open(name) } - catch { - case exn: Throwable => - GUI.error_dialog(view, "System error", GUI.scrollable_text(Exn.message(exn))) - }) - } - - override def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink = - new Hyperlink { def follow(view: View) = goto(view, name, line, column) } - override def hyperlink_command(snapshot: Document.Snapshot, command: Command, raw_offset: Int = 0) : Option[Hyperlink] = { @@ -174,4 +160,35 @@ } } } + + def hyperlink_command_id( + snapshot: Document.Snapshot, + id: Document_ID.Generic, + raw_offset: Text.Offset): Option[Hyperlink] = + { + snapshot.state.find_command(snapshot.version, id) match { + case Some((node, command)) => hyperlink_command(snapshot, command, raw_offset) + case None => None + } + } + + def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink = + new Hyperlink { def follow(view: View) = goto(view, name, line, column) } + + def hyperlink_source_file(name: String, line: Int): Option[Hyperlink] = + if (Path.is_ok(name)) + Isabelle_System.source_file(Path.explode(name)).map(path => + hyperlink_file(Isabelle_System.platform_path(path), line)) + else None + + def hyperlink_url(name: String): Hyperlink = + new Hyperlink { + def follow(view: View) = + default_thread_pool.submit(() => + try { Isabelle_System.open(name) } + catch { + case exn: Throwable => + GUI.error_dialog(view, "System error", GUI.scrollable_text(Exn.message(exn))) + }) + } } diff -r 7f229b0212fe -r 142139457653 src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Mon Mar 03 03:13:45 2014 +0100 +++ b/src/Tools/jEdit/src/rendering.scala Mon Mar 03 10:41:58 2014 +0100 @@ -327,20 +327,6 @@ /* hyperlinks */ - private def hyperlink_file(line: Int, name: String): Option[PIDE.editor.Hyperlink] = - if (Path.is_ok(name)) - Isabelle_System.source_file(Path.explode(name)).map(path => - PIDE.editor.hyperlink_file(Isabelle_System.platform_path(path), line)) - else None - - private def hyperlink_command(id: Document_ID.Generic, offset: Text.Offset) - : Option[PIDE.editor.Hyperlink] = - snapshot.state.find_command(snapshot.version, id) match { - case Some((node, command)) => - PIDE.editor.hyperlink_command(snapshot, command, offset) - case None => None - } - def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] = { snapshot.cumulate[Vector[Text.Info[PIDE.editor.Hyperlink]]]( @@ -364,8 +350,10 @@ val opt_link = props match { - case Position.Def_Line_File(line, name) => hyperlink_file(line, name) - case Position.Def_Id_Offset(id, offset) => hyperlink_command(id, offset) + case Position.Def_Line_File(line, name) => + PIDE.editor.hyperlink_source_file(name, line) + case Position.Def_Id_Offset(id, offset) => + PIDE.editor.hyperlink_command_id(snapshot, id, offset) case _ => None } opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link))) @@ -373,8 +361,10 @@ case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) => val opt_link = props match { - case Position.Line_File(line, name) => hyperlink_file(line, name) - case Position.Id_Offset(id, offset) => hyperlink_command(id, offset) + case Position.Line_File(line, name) => + PIDE.editor.hyperlink_source_file(name, line) + case Position.Id_Offset(id, offset) => + PIDE.editor.hyperlink_command_id(snapshot, id, offset) case _ => None } opt_link.map(link => links :+ (Text.Info(snapshot.convert(info_range), link)))