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