equal
deleted
inserted
replaced
18 /* document editor */ |
18 /* document editor */ |
19 |
19 |
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_editor_session: Option[Sessions.Background] = |
|
24 document_editor.value.session_background |
23 def document_editor_active: Boolean = |
25 def document_editor_active: Boolean = |
24 document_editor.value.is_active |
26 document_editor.value.is_active |
|
27 def document_editor_setup(background: Option[Sessions.Background]): Unit = |
|
28 document_editor.change(_.copy(session_background = background)) |
25 def document_editor_init(id: AnyRef): Unit = |
29 def document_editor_init(id: AnyRef): Unit = |
26 document_editor.change(_.register_view(id)) |
30 document_editor.change(_.register_view(id)) |
27 def document_editor_exit(id: AnyRef): Unit = |
31 def document_editor_exit(id: AnyRef): Unit = |
28 document_editor.change(_.unregister_view(id)) |
32 document_editor.change(_.unregister_view(id)) |
29 |
33 |