20 protected val document_editor: Synchronized[Document_Editor.State] = |
20 protected val document_editor: Synchronized[Document_Editor.State] = |
21 Synchronized(Document_Editor.State()) |
21 Synchronized(Document_Editor.State()) |
22 |
22 |
23 def document_session: Option[Sessions.Background] = document_editor.value.session_background |
23 def document_session: Option[Sessions.Background] = document_editor.value.session_background |
24 def document_active: Boolean = document_editor.value.is_active |
24 def document_active: Boolean = document_editor.value.is_active |
|
25 def document_active_changed(): Unit = {} |
|
26 private def document_editor_change(f: Document_Editor.State => Document_Editor.State): Unit = { |
|
27 val changed = |
|
28 document_editor.change_result { st => |
|
29 val st1 = f(st) |
|
30 (st.is_active != st1.is_active, st1) |
|
31 } |
|
32 if (changed) document_active_changed() |
|
33 } |
25 def document_setup(background: Option[Sessions.Background]): Unit = |
34 def document_setup(background: Option[Sessions.Background]): Unit = |
26 document_editor.change(_.copy(session_background = background)) |
35 document_editor_change(_.copy(session_background = background)) |
27 def document_init(id: AnyRef): Unit = document_editor.change(_.register_view(id)) |
36 def document_init(id: AnyRef): Unit = document_editor_change(_.register_view(id)) |
28 def document_exit(id: AnyRef): Unit = document_editor.change(_.unregister_view(id)) |
37 def document_exit(id: AnyRef): Unit = document_editor_change(_.unregister_view(id)) |
29 |
38 |
30 |
39 |
31 /* current situation */ |
40 /* current situation */ |
32 |
41 |
33 def current_node(context: Context): Option[Document.Node.Name] |
42 def current_node(context: Context): Option[Document.Node.Name] |