src/Pure/PIDE/editor.scala
author wenzelm
Mon, 12 Aug 2013 14:27:58 +0200
changeset 52977 15254e32d299
parent 52974 908e8a36e975
child 52978 37fbb3fde380
permissions -rw-r--r--
central management of Document.Overlays, independent of Document_Model;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
52971
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/PIDE/editor.scala
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
     3
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
     4
General editor operations.
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
     5
*/
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
     6
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
     7
package isabelle
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
     8
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
     9
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
    10
abstract class Editor[Context]
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
    11
{
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
    12
  def session: Session
52974
908e8a36e975 tuned signature;
wenzelm
parents: 52971
diff changeset
    13
  def flush(): Unit
52971
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
    14
  def current_context: Context
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
    15
  def current_node(context: Context): Option[Document.Node.Name]
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
    16
  def current_snapshot(context: Context): Option[Document.Snapshot]
52974
908e8a36e975 tuned signature;
wenzelm
parents: 52971
diff changeset
    17
  def node_snapshot(name: Document.Node.Name): Document.Snapshot
52971
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
    18
  def current_command(context: Context, snapshot: Document.Snapshot): Option[(Command, Text.Offset)]
52977
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52974
diff changeset
    19
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52974
diff changeset
    20
  def node_overlays(name: Document.Node.Name): Document.Node.Overlays
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52974
diff changeset
    21
  def insert_overlay(command: Command, fn: String, args: List[String]): Unit
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52974
diff changeset
    22
  def remove_overlay(command: Command, fn: String, args: List[String]): Unit
52971
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
    23
}
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
    24