author | wenzelm |
Mon, 12 Aug 2013 14:27:58 +0200 | |
changeset 52977 | 15254e32d299 |
parent 52974 | 908e8a36e975 |
child 52978 | 37fbb3fde380 |
permissions | -rw-r--r-- |
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 | 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 | 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 |