equal
deleted
inserted
replaced
13 def flush(): Unit |
13 def flush(): Unit |
14 def current_context: Context |
14 def current_context: Context |
15 def current_node(context: Context): Option[Document.Node.Name] |
15 def current_node(context: Context): Option[Document.Node.Name] |
16 def current_node_snapshot(context: Context): Option[Document.Snapshot] |
16 def current_node_snapshot(context: Context): Option[Document.Snapshot] |
17 def node_snapshot(name: Document.Node.Name): Document.Snapshot |
17 def node_snapshot(name: Document.Node.Name): Document.Snapshot |
18 def current_command(context: Context, snapshot: Document.Snapshot): Option[(Command, Text.Offset)] |
18 def current_command(context: Context, snapshot: Document.Snapshot): Option[Command] |
19 |
19 |
20 def node_overlays(name: Document.Node.Name): Document.Node.Overlays |
20 def node_overlays(name: Document.Node.Name): Document.Node.Overlays |
21 def insert_overlay(command: Command, fn: String, args: List[String]): Unit |
21 def insert_overlay(command: Command, fn: String, args: List[String]): Unit |
22 def remove_overlay(command: Command, fn: String, args: List[String]): Unit |
22 def remove_overlay(command: Command, fn: String, args: List[String]): Unit |
23 |
23 |