src/Pure/PIDE/editor.scala
author wenzelm
Mon Aug 12 12:06:48 2013 +0200 (2013-08-12 ago)
changeset 52974 908e8a36e975
parent 52971 31926d2c04ee
child 52977 15254e32d299
permissions -rw-r--r--
tuned signature;
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@52971
    12
  def session: Session
wenzelm@52974
    13
  def flush(): Unit
wenzelm@52971
    14
  def current_context: Context
wenzelm@52971
    15
  def current_node(context: Context): Option[Document.Node.Name]
wenzelm@52971
    16
  def current_snapshot(context: Context): Option[Document.Snapshot]
wenzelm@52974
    17
  def node_snapshot(name: Document.Node.Name): Document.Snapshot
wenzelm@52971
    18
  def current_command(context: Context, snapshot: Document.Snapshot): Option[(Command, Text.Offset)]
wenzelm@52971
    19
}
wenzelm@52971
    20