src/Pure/PIDE/editor.scala

   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]
+    focus: Boolean, snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0)
+      : Option[Hyperlink]
 }