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] }