equal
deleted
inserted
replaced
28 private var document_required = Set.empty[Document.Node.Name] |
28 private var document_required = Set.empty[Document.Node.Name] |
29 |
29 |
30 private def is_loaded_theory(name: Document.Node.Name): Boolean = |
30 private def is_loaded_theory(name: Document.Node.Name): Boolean = |
31 PIDE.resources.session_base.loaded_theory(name) |
31 PIDE.resources.session_base.loaded_theory(name) |
32 |
32 |
33 private def overall_node_status( |
33 private def overall_node_status(name: Document.Node.Name): Document_Status.Overall_Node_Status = { |
34 name: Document.Node.Name |
|
35 ): Document_Status.Overall_Node_Status.Value = { |
|
36 if (is_loaded_theory(name)) Document_Status.Overall_Node_Status.ok |
34 if (is_loaded_theory(name)) Document_Status.Overall_Node_Status.ok |
37 else nodes_status.overall_node_status(name) |
35 else nodes_status.overall_node_status(name) |
38 } |
36 } |
39 |
37 |
40 private def init_state(): Unit = GUI_Thread.require { |
38 private def init_state(): Unit = GUI_Thread.require { |