wenzelm@52971: /*  Title:      Pure/PIDE/editor.scala
wenzelm@52971:     Author:     Makarius
wenzelm@52971: 
wenzelm@52971: General editor operations.
wenzelm@52971: */
wenzelm@52971: 
wenzelm@52971: package isabelle
wenzelm@52971: 
wenzelm@52971: 
wenzelm@52971: abstract class Editor[Context]
wenzelm@52971: {
wenzelm@52971:   def session: Session
wenzelm@52974:   def flush(): Unit
wenzelm@54461:   def invoke(): Unit
wenzelm@52971:   def current_context: Context
wenzelm@52971:   def current_node(context: Context): Option[Document.Node.Name]
wenzelm@52978:   def current_node_snapshot(context: Context): Option[Document.Snapshot]
wenzelm@52974:   def node_snapshot(name: Document.Node.Name): Document.Snapshot
wenzelm@53844:   def current_command(context: Context, snapshot: Document.Snapshot): Option[Command]
wenzelm@52977: 
wenzelm@52977:   def node_overlays(name: Document.Node.Name): Document.Node.Overlays
wenzelm@52977:   def insert_overlay(command: Command, fn: String, args: List[String]): Unit
wenzelm@52977:   def remove_overlay(command: Command, fn: String, args: List[String]): Unit
wenzelm@52980: 
wenzelm@56494:   abstract class Hyperlink {
wenzelm@56494:     def external: Boolean
wenzelm@56494:     def follow(context: Context): Unit
wenzelm@56494:   }
wenzelm@52980:   def hyperlink_command(
wenzelm@55884:     snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0): Option[Hyperlink]
wenzelm@52971: }
wenzelm@52971: