src/Pure/PIDE/editor.scala
author wenzelm
Mon Feb 17 11:14:26 2014 +0100 (2014-02-17 ago)
changeset 55526 39708e59f4b0
parent 54702 3daeba5130f0
child 55876 142139457653
permissions -rw-r--r--
more markup;
     1 /*  Title:      Pure/PIDE/editor.scala
     2     Author:     Makarius
     3 
     4 General editor operations.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 abstract class Editor[Context]
    11 {
    12   def session: Session
    13   def flush(): Unit
    14   def invoke(): Unit
    15   def current_context: Context
    16   def current_node(context: Context): Option[Document.Node.Name]
    17   def current_node_snapshot(context: Context): Option[Document.Snapshot]
    18   def node_snapshot(name: Document.Node.Name): Document.Snapshot
    19   def current_command(context: Context, snapshot: Document.Snapshot): Option[Command]
    20 
    21   def node_overlays(name: Document.Node.Name): Document.Node.Overlays
    22   def insert_overlay(command: Command, fn: String, args: List[String]): Unit
    23   def remove_overlay(command: Command, fn: String, args: List[String]): Unit
    24 
    25   abstract class Hyperlink { def follow(context: Context): Unit }
    26   def hyperlink_url(name: String): Hyperlink
    27   def hyperlink_file(file_name: String, line: Int = 0, column: Int = 0): Hyperlink
    28   def hyperlink_command(
    29     snapshot: Document.Snapshot, command: Command, offset: Text.Offset = 0): Option[Hyperlink]
    30 }
    31