src/Pure/PIDE/editor.scala
changeset 64663 4c9fb4d4bca3
parent 64524 e6a3c55b929b
child 64664 951507563033
equal deleted inserted replaced
64662:5a2c15faf89c 64663:4c9fb4d4bca3
    22   def node_overlays(name: Document.Node.Name): Document.Node.Overlays
    22   def node_overlays(name: Document.Node.Name): Document.Node.Overlays
    23   def insert_overlay(command: Command, fn: String, args: List[String]): Unit
    23   def insert_overlay(command: Command, fn: String, args: List[String]): Unit
    24   def remove_overlay(command: Command, fn: String, args: List[String]): Unit
    24   def remove_overlay(command: Command, fn: String, args: List[String]): Unit
    25 
    25 
    26   abstract class Hyperlink {
    26   abstract class Hyperlink {
    27     def external: Boolean
    27     def external: Boolean = false
    28     def follow(context: Context): Unit
    28     def follow(context: Context): Unit
    29   }
    29   }
    30   def hyperlink_command(
    30   def hyperlink_command(
    31     focus: Boolean, snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0)
    31     focus: Boolean, snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0)
    32       : Option[Hyperlink]
    32       : Option[Hyperlink]