12 /* session */ |
12 /* session */ |
13 |
13 |
14 def session: Session |
14 def session: Session |
15 def flush(): Unit |
15 def flush(): Unit |
16 def invoke(): Unit |
16 def invoke(): Unit |
|
17 |
|
18 |
|
19 /* current situation */ |
|
20 |
17 def current_node(context: Context): Option[Document.Node.Name] |
21 def current_node(context: Context): Option[Document.Node.Name] |
18 def current_node_snapshot(context: Context): Option[Document.Snapshot] |
22 def current_node_snapshot(context: Context): Option[Document.Snapshot] |
19 def node_snapshot(name: Document.Node.Name): Document.Snapshot |
23 def node_snapshot(name: Document.Node.Name): Document.Snapshot |
20 def current_command(context: Context, snapshot: Document.Snapshot): Option[Command] |
24 def current_command(context: Context, snapshot: Document.Snapshot): Option[Command] |
21 |
25 |
22 |
26 |
23 /* overlays */ |
27 /* overlays */ |
24 |
28 |
25 private val overlays = Synchronized(Document.Overlays.empty) |
29 def node_overlays(name: Document.Node.Name): Document.Node.Overlays |
26 |
30 def insert_overlay(command: Command, fn: String, args: List[String]) |
27 def node_overlays(name: Document.Node.Name): Document.Node.Overlays = |
31 def remove_overlay(command: Command, fn: String, args: List[String]) |
28 overlays.value(name) |
|
29 |
|
30 def insert_overlay(command: Command, fn: String, args: List[String]): Unit = |
|
31 overlays.change(_.insert(command, fn, args)) |
|
32 |
|
33 def remove_overlay(command: Command, fn: String, args: List[String]): Unit = |
|
34 overlays.change(_.remove(command, fn, args)) |
|
35 |
32 |
36 |
33 |
37 /* hyperlinks */ |
34 /* hyperlinks */ |
38 |
35 |
39 abstract class Hyperlink |
36 abstract class Hyperlink |