# HG changeset patch
# User wenzelm
# Date 1671719006 -3600
# Node ID cb72b5996520f1d468ebe9015f332c5e31e1252c
# Parent  5a88237fac53499be6f9b03a5c3ac3a389308673
proper migrate_name between different kinds of Resources, notably for Windows;

diff -r 5a88237fac53 -r cb72b5996520 src/Pure/PIDE/document_editor.scala
--- a/src/Pure/PIDE/document_editor.scala	Thu Dec 22 08:56:16 2022 +0100
+++ b/src/Pure/PIDE/document_editor.scala	Thu Dec 22 15:23:26 2022 +0100
@@ -50,12 +50,6 @@
   ) {
     def is_active: Boolean = session_background.isDefined && views.nonEmpty
 
-    def is_required(name: Document.Node.Name): Boolean =
-      is_active && selection.contains(name) && all_document_theories.contains(name)
-
-    def required: List[Document.Node.Name] =
-      if (is_active) all_document_theories.filter(selection) else Nil
-
     def all_document_theories: List[Document.Node.Name] =
       session_background match {
         case Some(background) => background.base.all_document_theories
diff -r 5a88237fac53 -r cb72b5996520 src/Pure/PIDE/editor.scala
--- a/src/Pure/PIDE/editor.scala	Thu Dec 22 08:56:16 2022 +0100
+++ b/src/Pure/PIDE/editor.scala	Thu Dec 22 15:23:26 2022 +0100
@@ -29,17 +29,36 @@
         val st1 = f(st)
         val changed =
           st.active_document_theories != st1.active_document_theories ||
-          st.required != st1.required
+          st.selection != st1.selection
         (changed, st1)
       }
     if (changed) document_state_changed()
   }
 
   def document_session(): Option[Sessions.Background] = document_state().session_background
-  def document_required(): List[Document.Node.Name] = document_state().required
-  def document_node_required(name: Document.Node.Name): Boolean = document_state().is_required(name)
 
-  def document_theories(): List[Document.Node.Name] = document_state().active_document_theories
+  def document_required(): List[Document.Node.Name] = {
+    val st = document_state()
+    if (st.is_active) {
+      for {
+        a <- st.all_document_theories
+        b = session.resources.migrate_name(a)
+        if st.selection(b)
+      } yield b
+    }
+    else Nil
+  }
+
+  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)
+  }
+
+  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_setup(background: Option[Sessions.Background]): Unit =
@@ -52,7 +71,10 @@
   ): Unit = document_state_change(_.select(names, set = set, toggle = toggle))
 
   def document_select_all(set: Boolean = false): Unit =
-    document_state_change(st => st.select(st.active_document_theories, set = set))
+    document_state_change { st =>
+      val domain = st.active_document_theories.map(session.resources.migrate_name)
+      st.select(domain, 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 5a88237fac53 -r cb72b5996520 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Thu Dec 22 08:56:16 2022 +0100
+++ b/src/Pure/PIDE/resources.scala	Thu Dec 22 15:23:26 2022 +0100
@@ -70,6 +70,8 @@
 
   /* file-system operations */
 
+  def migrate_name(name: Document.Node.Name): Document.Node.Name = name
+
   def append(dir: String, source_path: Path): String =
     (Path.explode(dir) + source_path).expand.implode
 
diff -r 5a88237fac53 -r cb72b5996520 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Thu Dec 22 08:56:16 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Thu Dec 22 15:23:26 2022 +0100
@@ -100,6 +100,9 @@
       }
     }
 
+  override def migrate_name(standard_name: Document.Node.Name): Document.Node.Name =
+    node_name(Path.explode(standard_name.node).canonical_file)
+
   override def append(dir: String, source_path: Path): String = {
     val path = source_path.expand
     if (dir == "" || path.is_absolute) File.platform_path(path)
diff -r 5a88237fac53 -r cb72b5996520 src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Thu Dec 22 08:56:16 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Thu Dec 22 15:23:26 2022 +0100
@@ -50,6 +50,9 @@
     if (name.is_theory) Some(name) else None
   }
 
+  override def migrate_name(standard_name: Document.Node.Name): Document.Node.Name =
+    node_name(File.platform_path(Path.explode(standard_name.node).canonical))
+
   override def append(dir: String, source_path: Path): String = {
     val path = source_path.expand
     if (dir == "" || path.is_absolute) {