src/Pure/PIDE/editor.scala

--- a/src/Pure/PIDE/editor.scala	Tue Aug 11 15:24:49 2015 +0200
+++ b/src/Pure/PIDE/editor.scala	Tue Aug 11 17:00:16 2015 +0200
@@ -27,6 +27,7 @@
     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]
 }