author | wenzelm |
Sat, 21 Nov 2015 20:13:52 +0100 | |
changeset 61728 | 5f5ff1eab407 |
parent 60893 | 3c8b9b4b577c |
child 64521 | 1aef5a0e18d7 |
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 |
61728
5f5ff1eab407
double flush to ensure persistent "state" output is reset;
wenzelm
parents:
60893
diff
changeset
|
13 |
def flush(hidden: Boolean = true): Unit |
54461 | 14 |
def invoke(): Unit |
52971
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
15 |
def current_context: Context |
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
16 |
def current_node(context: Context): Option[Document.Node.Name] |
52978 | 17 |
def current_node_snapshot(context: Context): Option[Document.Snapshot] |
52974 | 18 |
def node_snapshot(name: Document.Node.Name): Document.Snapshot |
53844
71f103629327
skip ignored commands, similar to former proper_command_at (see d68ea01d5084) -- relevant to Output, Query_Operation etc.;
wenzelm
parents:
52980
diff
changeset
|
19 |
def current_command(context: Context, snapshot: Document.Snapshot): Option[Command] |
52977
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
20 |
|
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
21 |
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
|
22 |
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
|
23 |
def remove_overlay(command: Command, fn: String, args: List[String]): Unit |
52980 | 24 |
|
56494
1b74abf064e1
avoid confusion about pointless cursor movement with external links;
wenzelm
parents:
55884
diff
changeset
|
25 |
abstract class Hyperlink { |
1b74abf064e1
avoid confusion about pointless cursor movement with external links;
wenzelm
parents:
55884
diff
changeset
|
26 |
def external: Boolean |
1b74abf064e1
avoid confusion about pointless cursor movement with external links;
wenzelm
parents:
55884
diff
changeset
|
27 |
def follow(context: Context): Unit |
1b74abf064e1
avoid confusion about pointless cursor movement with external links;
wenzelm
parents:
55884
diff
changeset
|
28 |
} |
52980 | 29 |
def hyperlink_command( |
60893 | 30 |
focus: Boolean, snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0) |
31 |
: Option[Hyperlink] |
|
52971
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
32 |
} |
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
33 |