--- a/src/Pure/PIDE/document.scala Tue Jan 31 20:09:03 2023 +0100
+++ b/src/Pure/PIDE/document.scala Tue Jan 31 20:37:46 2023 +0100
@@ -589,7 +589,7 @@
def node_files: List[Node.Name] =
node_name :: node.load_commands.flatMap(_.blobs_names)
- def document_ready(name: Node.Name): Boolean =
+ def node_consolidated(name: Node.Name): Boolean =
state.node_consolidated(version, name)
--- a/src/Pure/PIDE/document_editor.scala Tue Jan 31 20:09:03 2023 +0100
+++ b/src/Pure/PIDE/document_editor.scala Tue Jan 31 20:37:46 2023 +0100
@@ -68,13 +68,16 @@
def register_view(id: AnyRef): State = copy(views = views + id)
def unregister_view(id: AnyRef): State = copy(views = views - id)
- def session(get_snapshot: () => Document.Snapshot): Session = {
+ def session(pide_session: isabelle.Session): Session = {
val background = session_background.filter(_.info.documents.nonEmpty)
val snapshot =
if (background.isEmpty) None
else {
- val snapshot = get_snapshot()
- if (snapshot.is_outdated || !selection.forall(snapshot.document_ready)) None
+ val snapshot = pide_session.snapshot()
+ def document_ready(name: Document.Node.Name): Boolean =
+ pide_session.resources.session_base.loaded_theory(name) ||
+ snapshot.node_consolidated(name)
+ if (snapshot.is_outdated || !selection.forall(document_ready)) None
else Some(snapshot)
}
Session(background, selection, snapshot)
--- a/src/Pure/PIDE/editor.scala Tue Jan 31 20:09:03 2023 +0100
+++ b/src/Pure/PIDE/editor.scala Tue Jan 31 20:37:46 2023 +0100
@@ -38,7 +38,7 @@
}
def document_session(): Document_Editor.Session =
- document_state().session(() => session.snapshot())
+ document_state().session(session)
def document_required(): List[Document.Node.Name] = {
val st = document_state()
--- a/src/Tools/jEdit/src/theories_status.scala Tue Jan 31 20:09:03 2023 +0100
+++ b/src/Tools/jEdit/src/theories_status.scala Tue Jan 31 20:37:46 2023 +0100
@@ -27,6 +27,16 @@
private var nodes_required = Set.empty[Document.Node.Name]
private var document_required = Set.empty[Document.Node.Name]
+ private def is_loaded_theory(name: Document.Node.Name): Boolean =
+ PIDE.resources.session_base.loaded_theory(name)
+
+ private def overall_node_status(
+ name: Document.Node.Name
+ ): Document_Status.Overall_Node_Status.Value = {
+ if (is_loaded_theory(name)) Document_Status.Overall_Node_Status.ok
+ else nodes_status.overall_node_status(name)
+ }
+
private def init_state(): Unit = GUI_Thread.require {
if (document) {
nodes_required = PIDE.editor.document_required().toSet
@@ -111,7 +121,9 @@
}
case None =>
- paint_segment(0, size.width, PIDE.options.color_value("unprocessed1_color"))
+ if (!is_loaded_theory(node_name)) {
+ paint_segment(0, size.width, PIDE.options.color_value("unprocessed1_color"))
+ }
}
super.paintComponent(gfx)
@@ -120,7 +132,7 @@
}
def label_border(name: Document.Node.Name): Unit = {
- val st = nodes_status.overall_node_status(name)
+ val st = overall_node_status(name)
val color =
st match {
case Document_Status.Overall_Node_Status.ok =>
@@ -203,7 +215,7 @@
}
else if (index >= 0 && node_renderer.in_label(index_location, point)) {
val name = listData(index)
- val st = nodes_status.overall_node_status(name)
+ val st = overall_node_status(name)
tooltip =
"theory " + quote(name.theory) +
(if (st == Document_Status.Overall_Node_Status.ok) "" else " (" + st + ")")