# HG changeset patch
# User wenzelm
# Date 1671453636 -3600
# Node ID 9dbf00b9c2d579a51b44df07ca355a7bd4b18d0a
# Parent  fdbdc573a06b2a8d5b432e375c28cba74646ffe8
clarified GUI;

diff -r fdbdc573a06b -r 9dbf00b9c2d5 src/Tools/jEdit/src/theories_status.scala
--- a/src/Tools/jEdit/src/theories_status.scala	Mon Dec 19 13:28:58 2022 +0100
+++ b/src/Tools/jEdit/src/theories_status.scala	Mon Dec 19 13:40:36 2022 +0100
@@ -51,6 +51,9 @@
   }
 
   private class Node_Renderer extends ListView.Renderer[Document.Node.Name] {
+    private val document_marker = Symbol.decode(" \\<^file>")
+    private val no_document_marker = "   "
+
     private object component extends BorderPanel {
       opaque = true
       border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
@@ -146,7 +149,10 @@
       component.required.selected =
         (if (document) document_required else theory_required).contains(name)
       component.label_border(name)
-      component.label.text = name.theory_base_name
+      component.label.text =
+        name.theory_base_name +
+        (if (!document && PIDE.editor.document_active && document_required.contains(name))
+          document_marker else no_document_marker)
       component
     }
   }