src/Pure/PIDE/editor.scala

--- a/src/Pure/PIDE/editor.scala	Wed Apr 09 12:33:02 2014 +0200
+++ b/src/Pure/PIDE/editor.scala	Wed Apr 09 13:32:34 2014 +0200
@@ -22,7 +22,10 @@
   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 }
+  abstract class Hyperlink {
+    def external: Boolean
+    def follow(context: Context): Unit
+  }
   def hyperlink_command(
     snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0): Option[Hyperlink]
 }