src/Pure/PIDE/editor.scala

--- a/src/Pure/PIDE/editor.scala	Mon Dec 09 09:44:57 2013 +0100
+++ b/src/Pure/PIDE/editor.scala	Mon Dec 09 12:16:52 2013 +0100
@@ -23,6 +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]