1/*  Title:      Pure/PIDE/editor.scala
2    Author:     Makarius
3
4General editor operations.
5*/
6
7package isabelle
8
9
10abstract 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}
54