src/Pure/PIDE/editor.scala
author wenzelm
Sun Mar 10 14:19:30 2019 +0100 (4 months ago ago)
changeset 70070 be04e9a053a7
parent 66101 0f0f294e314f
permissions -rw-r--r--
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
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@66082
    12
  /* session */
wenzelm@66082
    13
wenzelm@52971
    14
  def session: Session
wenzelm@66084
    15
  def flush(): Unit
wenzelm@54461
    16
  def invoke(): Unit
wenzelm@66101
    17
wenzelm@66101
    18
wenzelm@66101
    19
  /* current situation */
wenzelm@66101
    20
wenzelm@52971
    21
  def current_node(context: Context): Option[Document.Node.Name]
wenzelm@52978
    22
  def current_node_snapshot(context: Context): Option[Document.Snapshot]
wenzelm@52974
    23
  def node_snapshot(name: Document.Node.Name): Document.Snapshot
wenzelm@53844
    24
  def current_command(context: Context, snapshot: Document.Snapshot): Option[Command]
wenzelm@52977
    25
wenzelm@66082
    26
wenzelm@66082
    27
  /* overlays */
wenzelm@66082
    28
wenzelm@66101
    29
  def node_overlays(name: Document.Node.Name): Document.Node.Overlays
wenzelm@66101
    30
  def insert_overlay(command: Command, fn: String, args: List[String])
wenzelm@66101
    31
  def remove_overlay(command: Command, fn: String, args: List[String])
wenzelm@66082
    32
wenzelm@66082
    33
wenzelm@66082
    34
  /* hyperlinks */
wenzelm@52980
    35
wenzelm@66084
    36
  abstract class Hyperlink
wenzelm@66084
    37
  {
wenzelm@64663
    38
    def external: Boolean = false
wenzelm@56494
    39
    def follow(context: Context): Unit
wenzelm@56494
    40
  }
wenzelm@66084
    41
wenzelm@52980
    42
  def hyperlink_command(
wenzelm@64664
    43
    focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0)
wenzelm@60893
    44
      : Option[Hyperlink]
wenzelm@66094
    45
wenzelm@66094
    46
wenzelm@66094
    47
  /* dispatcher thread */
wenzelm@66094
    48
wenzelm@66094
    49
  def assert_dispatcher[A](body: => A): A
wenzelm@66094
    50
  def require_dispatcher[A](body: => A): A
wenzelm@66094
    51
  def send_dispatcher(body: => Unit): Unit
wenzelm@66094
    52
  def send_wait_dispatcher(body: => Unit): Unit
wenzelm@52971
    53
}