# HG changeset patch # User wenzelm # Date 1672428388 -3600 # Node ID a5ff9cf61551aca687f8fb2b367dd65ba36842a4 # Parent a150dd0ebdd31b61a3aa50e2dade01762e0e5f99 clarified generic path operations; diff -r a150dd0ebdd3 -r a5ff9cf61551 src/Pure/General/url.scala --- 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 diff -r a150dd0ebdd3 -r a5ff9cf61551 src/Pure/PIDE/command.scala --- 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) diff -r a150dd0ebdd3 -r a5ff9cf61551 src/Pure/PIDE/resources.scala --- 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 diff -r a150dd0ebdd3 -r a5ff9cf61551 src/Pure/Thy/file_format.scala --- 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 } diff -r a150dd0ebdd3 -r a5ff9cf61551 src/Pure/Thy/sessions.scala --- 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 } diff -r a150dd0ebdd3 -r a5ff9cf61551 src/Pure/Thy/thy_header.scala --- 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 */ diff -r a150dd0ebdd3 -r a5ff9cf61551 src/Pure/Tools/build_job.scala --- 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)