# HG changeset patch
# User wenzelm
# Date 1675193866 -3600
# Node ID 913c781ff6baff93825642f8f7fa49d07e5c401e
# Parent  158dfe7f68ed3654774544187528036e0b137df7
support document preparation from already loaded theories;

diff -r 158dfe7f68ed -r 913c781ff6ba src/Pure/PIDE/document.scala
--- 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)
 
 
diff -r 158dfe7f68ed -r 913c781ff6ba src/Pure/PIDE/document_editor.scala
--- 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)
diff -r 158dfe7f68ed -r 913c781ff6ba src/Pure/PIDE/editor.scala
--- 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()
diff -r 158dfe7f68ed -r 913c781ff6ba src/Tools/jEdit/src/theories_status.scala
--- 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 + ")")