tuned;

--- a/src/Pure/Admin/afp.scala	Tue Jan 03 15:32:54 2023 +0100
+++ b/src/Pure/Admin/afp.scala	Tue Jan 03 15:42:25 2023 +0100
@@ -93,7 +93,7 @@
 
     for ((line, i) <- split_lines(File.read(metadata_file)).zipWithIndex) {
       def err(msg: String): Nothing =
-        error(msg + Position.here(Position.Line_File(i + 1, metadata_file.expand.implode)))
+        error(msg + Position.here(Position.Line_File(i + 1, File.standard_path(metadata_file))))
 
       line match {
         case Section(name) => flush(); section = name

--- a/src/Pure/Admin/build_release.scala	Tue Jan 03 15:32:54 2023 +0100
+++ b/src/Pure/Admin/build_release.scala	Tue Jan 03 15:42:25 2023 +0100
@@ -425,7 +425,7 @@
 
       Isabelle_System.new_directory(context.dist_dir)
 
-      hg.archive(context.isabelle_dir.expand.implode, rev = id)
+      hg.archive(File.standard_path(context.isabelle_dir), rev = id)
 
       for (name <- List(".hg_archival.txt", ".hgtags", ".hgignore", "README_REPOSITORY")) {
         (context.isabelle_dir + Path.explode(name)).file.delete

--- a/src/Pure/Admin/jenkins.scala	Tue Jan 03 15:32:54 2023 +0100
+++ b/src/Pure/Admin/jenkins.scala	Tue Jan 03 15:42:25 2023 +0100
@@ -101,7 +101,7 @@
       val log_path = log_dir + log_filename.xz
 
       if (!log_path.is_file) {
-        progress.echo(log_path.expand.implode)
+        progress.echo(File.standard_path(log_path))
         Isabelle_System.make_directory(log_dir)
 
         val ml_statistics =

--- a/src/Pure/General/mercurial.scala	Tue Jan 03 15:32:54 2023 +0100
+++ b/src/Pure/General/mercurial.scala	Tue Jan 03 15:42:25 2023 +0100
@@ -53,7 +53,7 @@
       root + (if (raw) "/raw-rev/" else "/rev/") + rev
 
     def file(path: Path, rev: String = "tip", raw: Boolean = false): String =
-      root + (if (raw) "/raw-file/" else "/file/") + rev + "/" + path.expand.implode
+      root + (if (raw) "/raw-file/" else "/file/") + rev + "/" + File.standard_path(path)
 
     def archive(rev: String = "tip"): String =
       root + "/archive/" + rev + ".tar.gz"

--- a/src/Pure/PIDE/resources.scala	Tue Jan 03 15:32:54 2023 +0100
+++ b/src/Pure/PIDE/resources.scala	Tue Jan 03 15:42:25 2023 +0100
@@ -73,7 +73,7 @@
   def migrate_name(name: Document.Node.Name): Document.Node.Name = name
 
   def append_path(prefix: String, source_path: Path): String =
-    (Path.explode(prefix) + source_path).expand.implode
+    File.standard_path(Path.explode(prefix) + source_path)
 
 
   /* source files of Isabelle/ML bootstrap */

--- a/src/Pure/Thy/sessions.scala	Tue Jan 03 15:32:54 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Tue Jan 03 15:42:25 2023 +0100
@@ -706,7 +706,7 @@
         if File.is_bib(file.file_name)
       } yield {
         val path = dir + document_dir + file
-        Bibtex.Entries.parse(File.read(path), file_pos = path.expand.implode)
+        Bibtex.Entries.parse(File.read(path), file_pos = File.standard_path(path))
       }).foldRight(Bibtex.Entries.empty)(_ ::: _)
 
     def record_proofs: Boolean = options.int("record_proofs") >= 2
@@ -1450,7 +1450,7 @@
     def the_heap(name: String): Path =
       find_heap(name) getOrElse
         error("Missing heap image for session " + quote(name) + " -- expected in:\n" +
-          cat_lines(input_dirs.map(dir => "  " + dir.expand.implode)))
+          cat_lines(input_dirs.map(dir => "  " + File.standard_path(dir))))
 
 
     /* database */

--- a/src/Pure/Tools/build.scala	Tue Jan 03 15:32:54 2023 +0100
+++ b/src/Pure/Tools/build.scala	Tue Jan 03 15:42:25 2023 +0100
@@ -253,7 +253,7 @@
         case Nil =>
         case unknown_files =>
           progress.echo_warning("Unknown files (not part of the underlying Mercurial repository):" +
-            unknown_files.map(path => path.expand.implode).sorted.mkString("\n  ", "\n  ", ""))
+            unknown_files.map(File.standard_path).sorted.mkString("\n  ", "\n  ", ""))
       }
     }
 

--- a/src/Pure/Tools/check_keywords.scala	Tue Jan 03 15:32:54 2023 +0100
+++ b/src/Pure/Tools/check_keywords.scala	Tue Jan 03 15:42:25 2023 +0100
@@ -35,7 +35,8 @@
     check: Set[String],
     paths: List[Path]
   ): Unit = {
-    val parallel_args = paths.map(path => (File.read(path), Token.Pos.file(path.expand.implode)))
+    val parallel_args =
+      paths.map(path => (File.read(path), Token.Pos.file(File.standard_path(path))))
 
     val bad =
       Par_List.map({ (arg: (String, Token.Pos)) =>

--- a/src/Pure/Tools/logo.scala	Tue Jan 03 15:32:54 2023 +0100
+++ b/src/Pure/Tools/logo.scala	Tue Jan 03 15:42:25 2023 +0100
@@ -23,7 +23,7 @@
       Isabelle_System.bash(
         "\"$ISABELLE_EPSTOPDF\" --filter < " + File.bash_path(tmp_file) +
           " > " + File.bash_path(output_file)).check
-      if (!quiet) Output.writeln(output_file.expand.implode)
+      if (!quiet) Output.writeln(File.standard_path(output_file))
     }
   }
 

--- a/src/Tools/VSCode/src/build_vscode_extension.scala	Tue Jan 03 15:32:54 2023 +0100
+++ b/src/Tools/VSCode/src/build_vscode_extension.scala	Tue Jan 03 15:42:25 2023 +0100
@@ -24,7 +24,7 @@
       Sessions.background(options, logic, dirs = dirs).check_errors.base.overall_syntax.keywords
 
     val output_path = build_dir + Path.explode("isabelle-grammar.json")
-    progress.echo(output_path.expand.implode)
+    progress.echo(File.standard_path(output_path))
 
     val (minor_keywords, operators) =
       keywords.minor.iterator.toList.partition(Symbol.is_ascii_identifier)