src/Pure/PIDE/editor.scala
author wenzelm
Mon Mar 13 21:37:35 2017 +0100 (2017-03-13 ago)
changeset 65214 a2ec0db555c7
parent 64867 e7220f4de11f
child 66082 2d12a730a380
permissions -rw-r--r--
clarified modules;
wenzelm@52971
     1
/*  Title:      Pure/PIDE/editor.scala
wenzelm@52971
     2
    Author:     Makarius
wenzelm@52971
     3
wenzelm@52971
     4
General editor operations.
wenzelm@52971
     5
*/
wenzelm@52971
     6
wenzelm@52971
     7
package isabelle
wenzelm@52971
     8
wenzelm@52971
     9
wenzelm@52971
    10
abstract class Editor[Context]
wenzelm@52971
    11
{
wenzelm@52971
    12
  def session: Session
wenzelm@64867
    13
  def flush(hidden: Boolean = false, purge: Boolean = false): Unit
wenzelm@54461
    14
  def invoke(): Unit
wenzelm@64524
    15
  def invoke_generated(): Unit
wenzelm@52971
    16
  def current_context: Context
wenzelm@52971
    17
  def current_node(context: Context): Option[Document.Node.Name]
wenzelm@52978
    18
  def current_node_snapshot(context: Context): Option[Document.Snapshot]
wenzelm@52974
    19
  def node_snapshot(name: Document.Node.Name): Document.Snapshot
wenzelm@53844
    20
  def current_command(context: Context, snapshot: Document.Snapshot): Option[Command]
wenzelm@52977
    21
wenzelm@52977
    22
  def node_overlays(name: Document.Node.Name): Document.Node.Overlays
wenzelm@52977
    23
  def insert_overlay(command: Command, fn: String, args: List[String]): Unit
wenzelm@52977
    24
  def remove_overlay(command: Command, fn: String, args: List[String]): Unit
wenzelm@52980
    25
wenzelm@56494
    26
  abstract class Hyperlink {
wenzelm@64663
    27
    def external: Boolean = false
wenzelm@56494
    28
    def follow(context: Context): Unit
wenzelm@56494
    29
  }
wenzelm@52980
    30
  def hyperlink_command(
wenzelm@64664
    31
    focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0)
wenzelm@60893
    32
      : Option[Hyperlink]
wenzelm@52971
    33
}
wenzelm@52971
    34