clarified generic path operations;

--- a/src/Pure/General/url.scala	Fri Dec 30 16:23:32 2022 +0100
+++ b/src/Pure/General/url.scala	Fri Dec 30 20:26:28 2022 +0100
@@ -104,6 +104,25 @@
 
   /* generic path notation: local, ssh, rsync, ftp, http */
 
+  private val separators1 = "/\\"
+  private val separators2 = ":/\\"
+
+  def is_base_name(s: String, suffix: String = ""): Boolean =
+    s.nonEmpty && !s.exists(separators2.contains) && s.endsWith(suffix)
+
+  def get_base_name(s: String, suffix: String = ""): Option[String] = {
+    val i = s.lastIndexWhere(separators2.contains)
+    if (i + 1 >= s.length) None else Library.try_unsuffix(suffix, s.substring(i + 1))
+  }
+
+  def strip_base_name(s: String, suffix: String = ""): Option[String] = {
+    val i = s.lastIndexWhere(separators2.contains)
+    val j = s.lastIndexWhere(c => !separators1.contains(c), end = i)
+    if (i + 1 >= s.length || !s.endsWith(suffix)) None
+    else if (j < 0) Some(s.substring(0, i + 1))
+    else Some(s.substring(0, j + 1))
+  }
+
   def append_path(prefix: String, suffix: String): String =
     if (prefix.endsWith(":") || prefix.endsWith("/") || prefix.endsWith("\\") || prefix.isEmpty) {
       prefix + suffix

--- a/src/Pure/PIDE/command.scala	Fri Dec 30 16:23:32 2022 +0100
+++ b/src/Pure/PIDE/command.scala	Fri Dec 30 20:26:28 2022 +0100
@@ -450,7 +450,7 @@
           for { ((import_name, pos), s) <- imports_pos zip raw_imports if !can_import(import_name) }
           yield {
             val completion =
-              if (Thy_Header.is_base_name(s)) resources.complete_import_name(node_name, s) else Nil
+              if (Url.is_base_name(s)) resources.complete_import_name(node_name, s) else Nil
             "Bad theory import " +
               Markup.Path(import_name.node).markup(quote(import_name.toString)) +
               Position.here(pos) + Completion.report_theories(pos, completion)

--- a/src/Pure/PIDE/resources.scala	Fri Dec 30 16:23:32 2022 +0100
+++ b/src/Pure/PIDE/resources.scala	Fri Dec 30 20:26:28 2022 +0100
@@ -172,7 +172,7 @@
     val theory = theory_name(qualifier, Thy_Header.import_name(s))
     val literal_import =
       literal_theory(theory) && qualifier != sessions_structure.theory_qualifier(theory)
-    if (literal_import && !Thy_Header.is_base_name(s)) {
+    if (literal_import && !Url.is_base_name(s)) {
       error("Bad import of theory from other session via file-path: " + quote(s))
     }
     if (session_base.loaded_theory(theory)) loaded_theory_node(theory)
@@ -180,7 +180,7 @@
       find_theory_node(theory) match {
         case Some(node_name) => node_name
         case None =>
-          if (Thy_Header.is_base_name(s) && literal_theory(s)) loaded_theory_node(theory)
+          if (Url.is_base_name(s) && literal_theory(s)) loaded_theory_node(theory)
           else file_node(Path.explode(s).thy, dir = dir, theory = theory)
       }
     }
@@ -210,7 +210,7 @@
     (for {
       (session, (info, _))  <- sessions_structure.imports_graph.iterator
       dir <- (if (session == context_session) context_dir.toList else info.dirs).iterator
-      theory <- Thy_Header.try_read_dir(dir).iterator
+      theory <- Thy_Header.list_thy_names(dir).iterator
       if Completion.completed(s)(theory)
     } yield {
       if (session == context_session || global_theory(theory)) theory

--- a/src/Pure/Thy/file_format.scala	Fri Dec 30 16:23:32 2022 +0100
+++ b/src/Pure/Thy/file_format.scala	Fri Dec 30 20:26:28 2022 +0100
@@ -80,7 +80,7 @@
     name: Document.Node.Name
   ): Option[Document.Node.Name] = {
     for {
-      (_, thy) <- Thy_Header.split_file_name(name.node)
+      thy <- Url.get_base_name(name.node)
       if detect(name.node) && theory_suffix.nonEmpty
     }
     yield {
@@ -91,9 +91,10 @@
 
   def make_theory_content(resources: Resources, thy_name: Document.Node.Name): Option[String] = {
     for {
-      (prefix, suffix) <- Thy_Header.split_file_name(thy_name.node)
+      prefix <- Url.strip_base_name(thy_name.node)
+      suffix <- Url.get_base_name(thy_name.node)
       if detect(prefix) && suffix == theory_suffix
-      (_, thy) <- Thy_Header.split_file_name(prefix)
+      thy <- Url.get_base_name(prefix)
       s <- proper_string(theory_content(thy))
     } yield s
   }

--- a/src/Pure/Thy/sessions.scala	Fri Dec 30 16:23:32 2022 +0100
+++ b/src/Pure/Thy/sessions.scala	Fri Dec 30 20:26:28 2022 +0100
@@ -42,8 +42,8 @@
     val file_ext = ""
 
     override def detect(name: String): Boolean =
-      Thy_Header.split_file_name(name) match {
-        case Some((_, file_name)) => file_name == roots_name
+      Url.get_base_name(name) match {
+        case Some(base_name) => base_name == roots_name
         case None => false
       }
 

--- a/src/Pure/Thy/thy_header.scala	Fri Dec 30 16:23:32 2022 +0100
+++ b/src/Pure/Thy/thy_header.scala	Fri Dec 30 20:26:28 2022 +0100
@@ -76,32 +76,31 @@
   val bootstrap_global_theories =
     (Sessions.root_name :: (ml_roots ::: bootstrap_thys).map(_._2)).map(_ -> PURE)
 
-  private val Thy_File_Name = new Regex(""".*?([^/\\:]+)\.thy""")
-  private val Split_File_Name = new Regex("""(.*?)[/\\]*([^/\\:]+)""")
-  private val File_Name = new Regex(""".*?([^/\\:]+)""")
-
-  def is_base_name(s: String): Boolean =
-    s != "" && !s.exists("/\\:".contains(_))
-
-  def split_file_name(s: String): Option[(String, String)] =
-    s match {
-      case Split_File_Name(s1, s2) => Some((s1, s2))
-      case _ => None
-    }
-
   def import_name(s: String): String =
-    s match {
-      case File_Name(name) if !File.is_thy(name) => name
+    Url.get_base_name(s) match {
+      case Some(name) if !File.is_thy(name) => name
       case _ => error("Malformed theory import: " + quote(s))
     }
 
+  def get_thy_name(s: String): Option[String] = Url.get_base_name(s, suffix = ".thy")
+
+  def list_thy_names(dir: Path): List[String] = {
+    val files =
+      try { File.read_dir(dir) }
+      catch { case ERROR(_) => Nil }
+    files.flatMap(get_thy_name)
+  }
+
   def theory_name(s: String): String =
-    s match {
-      case Thy_File_Name(name) => bootstrap_name(name)
-      case File_Name(name) =>
-        if (name == Sessions.root_name) name
-        else ml_roots.collectFirst({ case (a, b) if a == name => b }).getOrElse("")
-      case _ => ""
+    get_thy_name(s) match {
+      case Some(name) => bootstrap_name(name)
+      case None =>
+        Url.get_base_name(s) match {
+          case Some(name) =>
+            if (name == Sessions.root_name) name
+            else ml_roots.collectFirst({ case (a, b) if a == name => b }).getOrElse("")
+          case None => ""
+        }
     }
 
   def is_ml_root(theory: String): Boolean =
@@ -113,13 +112,6 @@
   def bootstrap_name(theory: String): String =
     bootstrap_thys.collectFirst({ case (a, b) if a == theory => b }).getOrElse(theory)
 
-  def try_read_dir(dir: Path): List[String] = {
-    val files =
-      try { File.read_dir(dir) }
-      catch { case ERROR(_) => Nil }
-    for { Thy_File_Name(name) <- files } yield name
-  }
-
 
   /* parser */
 

--- a/src/Pure/Tools/build_job.scala	Fri Dec 30 16:23:32 2022 +0100
+++ b/src/Pure/Tools/build_job.scala	Fri Dec 30 20:26:28 2022 +0100
@@ -31,10 +31,8 @@
     }
     yield {
       val master_dir =
-        Thy_Header.split_file_name(thy_file) match {
-          case Some((dir, _)) => dir
-          case None => error("Cannot determine theory master directory: " + quote(thy_file))
-        }
+        Url.strip_base_name(thy_file).getOrElse(
+          error("Cannot determine theory master directory: " + quote(thy_file)))
       val node_name =
         Document.Node.Name(thy_file, master_dir = master_dir, theory = theory_context.theory)