equal
deleted
inserted
replaced
10 abstract class Editor[Context] |
10 abstract class Editor[Context] |
11 { |
11 { |
12 /* session */ |
12 /* session */ |
13 |
13 |
14 def session: Session |
14 def session: Session |
15 def flush(hidden: Boolean = false, purge: Boolean = false): Unit |
15 def flush(): Unit |
16 def invoke(): Unit |
16 def invoke(): Unit |
17 def current_node(context: Context): Option[Document.Node.Name] |
17 def current_node(context: Context): Option[Document.Node.Name] |
18 def current_node_snapshot(context: Context): Option[Document.Snapshot] |
18 def current_node_snapshot(context: Context): Option[Document.Snapshot] |
19 def node_snapshot(name: Document.Node.Name): Document.Snapshot |
19 def node_snapshot(name: Document.Node.Name): Document.Snapshot |
20 def current_command(context: Context, snapshot: Document.Snapshot): Option[Command] |
20 def current_command(context: Context, snapshot: Document.Snapshot): Option[Command] |
34 overlays.change(_.remove(command, fn, args)) |
34 overlays.change(_.remove(command, fn, args)) |
35 |
35 |
36 |
36 |
37 /* hyperlinks */ |
37 /* hyperlinks */ |
38 |
38 |
39 abstract class Hyperlink { |
39 abstract class Hyperlink |
|
40 { |
40 def external: Boolean = false |
41 def external: Boolean = false |
41 def follow(context: Context): Unit |
42 def follow(context: Context): Unit |
42 } |
43 } |
|
44 |
43 def hyperlink_command( |
45 def hyperlink_command( |
44 focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0) |
46 focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0) |
45 : Option[Hyperlink] |
47 : Option[Hyperlink] |
46 } |
48 } |
47 |
|