src/Pure/PIDE/editor.scala
changeset 64664 951507563033
parent 64663 4c9fb4d4bca3
child 64866 372c833c7660
--- a/src/Pure/PIDE/editor.scala	Fri Dec 23 15:53:53 2016 +0100
+++ b/src/Pure/PIDE/editor.scala	Fri Dec 23 16:20:42 2016 +0100
@@ -28,7 +28,7 @@
     def follow(context: Context): Unit
   }
   def hyperlink_command(
-    focus: Boolean, snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0)
+    focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0)
       : Option[Hyperlink]
 }