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";
     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   /* session */
    13 
    14   def session: Session
    15   def flush(): Unit
    16   def invoke(): Unit
    17 
    18 
    19   /* current situation */
    20 
    21   def current_node(context: Context): Option[Document.Node.Name]
    22   def current_node_snapshot(context: Context): Option[Document.Snapshot]
    23   def node_snapshot(name: Document.Node.Name): Document.Snapshot
    24   def current_command(context: Context, snapshot: Document.Snapshot): Option[Command]
    25 
    26 
    27   /* overlays */
    28 
    29   def node_overlays(name: Document.Node.Name): Document.Node.Overlays
    30   def insert_overlay(command: Command, fn: String, args: List[String])
    31   def remove_overlay(command: Command, fn: String, args: List[String])
    32 
    33 
    34   /* hyperlinks */
    35 
    36   abstract class Hyperlink
    37   {
    38     def external: Boolean = false
    39     def follow(context: Context): Unit
    40   }
    41 
    42   def hyperlink_command(
    43     focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0)
    44       : Option[Hyperlink]
    45 
    46 
    47   /* dispatcher thread */
    48 
    49   def assert_dispatcher[A](body: => A): A
    50   def require_dispatcher[A](body: => A): A
    51   def send_dispatcher(body: => Unit): Unit
    52   def send_wait_dispatcher(body: => Unit): Unit
    53 }