# HG changeset patch
# User wenzelm
# Date 1675609158 -3600
# Node ID a541da01ba67e8f113130b670cda19b9c08cba64
# Parent  3d709d300d0f02b61f49af76b36bfe9ff489c80d
clarified signature selection: SortedSet[String], which fits better to stored json and works properly on Windows (NB: document theories have an authentic session-theory name);

diff -r 3d709d300d0f -r a541da01ba67 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sun Feb 05 15:01:49 2023 +0100
+++ b/src/Pure/PIDE/document.scala	Sun Feb 05 15:59:18 2023 +0100
@@ -592,6 +592,12 @@
     def node_consolidated(name: Node.Name): Boolean =
       state.node_consolidated(version, name)
 
+    def theory_consolidated(theory: String): Boolean =
+      version.nodes.theory_name(theory) match {
+        case Some(name) => node_consolidated(name)
+        case None => false
+      }
+
 
     /* pending edits */
 
diff -r 3d709d300d0f -r a541da01ba67 src/Pure/PIDE/document_editor.scala
--- a/src/Pure/PIDE/document_editor.scala	Sun Feb 05 15:01:49 2023 +0100
+++ b/src/Pure/PIDE/document_editor.scala	Sun Feb 05 15:59:18 2023 +0100
@@ -7,6 +7,9 @@
 package isabelle
 
 
+import scala.collection.immutable.SortedSet
+
+
 object Document_Editor {
   /* document output */
 
@@ -26,7 +29,7 @@
           pdf <- JSON.string(json, "pdf")
         } yield {
           Meta_Data(name,
-            selection,
+            SortedSet.from(selection),
             SHA1.fake_digest(sources),
             SHA1.fake_digest(log),
             SHA1.fake_digest(pdf))
@@ -36,13 +39,13 @@
     }
 
     def write(
-      selection: Set[Document.Node.Name],
+      selection: SortedSet[String],
       doc: Document_Build.Document_Output,
       name: String = document_name
     ): Unit = {
       val json =
         JSON.Object(
-          "selection" -> selection.toList.map(_.theory).sorted,
+          "selection" -> selection.toList,
           "sources" -> doc.sources.toString,
           "log" -> SHA1.digest(doc.log).toString,
           "pdf" -> SHA1.digest(doc.pdf).toString)
@@ -52,7 +55,7 @@
 
   sealed case class Meta_Data(
     name: String,
-    selection: List[String],
+    selection: SortedSet[String],
     sources: SHA1.Digest,
     log: SHA1.Digest,
     pdf: SHA1.Digest
@@ -67,7 +70,7 @@
   }
 
   def write_document(
-    selection: Set[Document.Node.Name],
+    selection: SortedSet[String],
     doc: Document_Build.Document_Output,
     name: String = document_name
   ): Unit = {
@@ -87,7 +90,7 @@
 
   sealed case class Session(
     background: Option[Sessions.Background],
-    selection: Set[Document.Node.Name],
+    selection: SortedSet[String],
     snapshot: Option[Document.Snapshot]
   ) {
     def is_vacuous: Boolean = background.isEmpty
@@ -101,7 +104,7 @@
 
   sealed case class State(
     session_background: Option[Sessions.Background] = None,
-    selection: Set[Document.Node.Name] = Set.empty,
+    selection: SortedSet[String] = SortedSet.empty,
     views: Set[AnyRef] = Set.empty,
   ) {
     def is_active: Boolean = session_background.isDefined && views.nonEmpty
@@ -116,15 +119,15 @@
       if (is_active) all_document_theories else Nil
 
     def select(
-      names: Iterable[Document.Node.Name],
+      theories: Iterable[String],
       set: Boolean = false,
       toggle: Boolean = false
     ): State = {
       copy(selection =
-        names.foldLeft(selection) {
-          case (sel, name) =>
-            val b = if (toggle) !selection(name) else set
-            if (b) sel + name else sel - name
+        theories.foldLeft(selection) {
+          case (sel, theory) =>
+            val b = if (toggle) !selection(theory) else set
+            if (b) sel + theory else sel - theory
         })
     }
 
@@ -137,9 +140,9 @@
         if (background.isEmpty) None
         else {
           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)
+          def document_ready(theory: String): Boolean =
+            pide_session.resources.session_base.loaded_theory(theory) ||
+            snapshot.theory_consolidated(theory)
           if (snapshot.is_outdated || !selection.forall(document_ready)) None
           else Some(snapshot)
         }
diff -r 3d709d300d0f -r a541da01ba67 src/Pure/PIDE/editor.scala
--- a/src/Pure/PIDE/editor.scala	Sun Feb 05 15:01:49 2023 +0100
+++ b/src/Pure/PIDE/editor.scala	Sun Feb 05 15:59:18 2023 +0100
@@ -46,7 +46,7 @@
       for {
         a <- st.all_document_theories
         b = session.resources.migrate_name(a)
-        if st.selection(b)
+        if st.selection(b.theory)
       } yield b
     }
     else Nil
@@ -55,29 +55,27 @@
   def document_node_required(name: Document.Node.Name): Boolean = {
     val st = document_state()
     st.is_active &&
-    st.selection.contains(name) &&
-    st.all_document_theories.exists(a => session.resources.migrate_name(a) == name)
+    st.selection.contains(name.theory) &&
+    st.all_document_theories.exists(a => a.theory == name.theory)
   }
 
   def document_theories(): List[Document.Node.Name] =
     document_state().active_document_theories.map(session.resources.migrate_name)
 
-  def document_selection(): Set[Document.Node.Name] = document_state().selection
+  def document_selection(): Set[String] = document_state().selection
 
   def document_setup(background: Option[Sessions.Background]): Unit =
     document_state_change(_.copy(session_background = background))
 
   def document_select(
-    names: Iterable[Document.Node.Name],
+    theories: Iterable[String],
     set: Boolean = false,
     toggle: Boolean = false
-  ): Unit = document_state_change(_.select(names, set = set, toggle = toggle))
+  ): Unit = document_state_change(_.select(theories, set = set, toggle = toggle))
 
   def document_select_all(set: Boolean = false): Unit =
-    document_state_change { st =>
-      val domain = st.active_document_theories.map(session.resources.migrate_name)
-      st.select(domain, set = set)
-    }
+    document_state_change(st =>
+      st.select(st.active_document_theories.map(_.theory), set = set))
 
   def document_init(id: AnyRef): Unit = document_state_change(_.register_view(id))
   def document_exit(id: AnyRef): Unit = document_state_change(_.unregister_view(id))
diff -r 3d709d300d0f -r a541da01ba67 src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Sun Feb 05 15:01:49 2023 +0100
+++ b/src/Pure/Thy/document_build.scala	Sun Feb 05 15:59:18 2023 +0100
@@ -159,14 +159,14 @@
   def context(
     session_context: Export.Session_Context,
     document_session: Option[Sessions.Base] = None,
-    document_selection: Document.Node.Name => Boolean = _ => true,
+    document_selection: String => Boolean = _ => true,
     progress: Progress = new Progress
   ): Context = new Context(session_context, document_session, document_selection, progress)
 
   final class Context private[Document_Build](
     val session_context: Export.Session_Context,
     document_session: Option[Sessions.Base],
-    document_selection: Document.Node.Name => Boolean,
+    document_selection: String => Boolean,
     val progress: Progress
   ) {
     context =>
@@ -236,7 +236,7 @@
     lazy val document_latex: List[Document_Latex] =
       for (name <- all_document_theories)
       yield {
-        val selected = document_selection(name)
+        val selected = document_selection(name.theory)
 
         val body =
           if (selected) {
diff -r 3d709d300d0f -r a541da01ba67 src/Tools/jEdit/src/theories_status.scala
--- a/src/Tools/jEdit/src/theories_status.scala	Sun Feb 05 15:01:49 2023 +0100
+++ b/src/Tools/jEdit/src/theories_status.scala	Sun Feb 05 15:59:18 2023 +0100
@@ -199,7 +199,7 @@
           if (node_renderer.in_required(index_location, point)) {
             if (clicks == 1) {
               val name = listData(index)
-              if (document) PIDE.editor.document_select(Set(name), toggle = true)
+              if (document) PIDE.editor.document_select(Set(name.theory), toggle = true)
               else Document_Model.node_required(name, toggle = true)
             }
           }