# HG changeset patch # User wenzelm # Date 1672756945 -3600 # Node ID 186e07be32c395356e996e343a79a84fb2dd7b39 # Parent d9913b41a7bc52772ca60d20f4f6d3b029f07eec tuned; diff -r d9913b41a7bc -r 186e07be32c3 src/Pure/Admin/afp.scala --- 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 diff -r d9913b41a7bc -r 186e07be32c3 src/Pure/Admin/build_release.scala --- 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 diff -r d9913b41a7bc -r 186e07be32c3 src/Pure/Admin/jenkins.scala --- 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 = diff -r d9913b41a7bc -r 186e07be32c3 src/Pure/General/mercurial.scala --- 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" diff -r d9913b41a7bc -r 186e07be32c3 src/Pure/PIDE/resources.scala --- 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 */ diff -r d9913b41a7bc -r 186e07be32c3 src/Pure/Thy/sessions.scala --- 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 */ diff -r d9913b41a7bc -r 186e07be32c3 src/Pure/Tools/build.scala --- 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 ", "")) } } diff -r d9913b41a7bc -r 186e07be32c3 src/Pure/Tools/check_keywords.scala --- 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)) => diff -r d9913b41a7bc -r 186e07be32c3 src/Pure/Tools/logo.scala --- 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)) } } diff -r d9913b41a7bc -r 186e07be32c3 src/Tools/VSCode/src/build_vscode_extension.scala --- 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)