# HG changeset patch # User wenzelm # Date 1672777344 -3600 # Node ID 7fd3e461d3b642301bc1fd320ffbe5028bbffe32 # Parent b3c5bc06f5be3c203fedf1d8dcdb166003a72955# Parent 5786d6394659d99dfa18feb5871d40a7c29b6b67 merged diff -r b3c5bc06f5be -r 7fd3e461d3b6 src/HOL/Library/code_test.ML --- a/src/HOL/Library/code_test.ML Tue Jan 03 18:23:52 2023 +0100 +++ b/src/HOL/Library/code_test.ML Tue Jan 03 21:22:24 2023 +0100 @@ -316,8 +316,8 @@ {environment = ML_Env.SML, redirect = false, verbose = false, debug = NONE, writeln = writeln, warning = warning} Position.none - (ML_Lex.read_text (code, Path.position code_path) @ - ML_Lex.read_text (driver, Path.position driver_path) @ + (ML_Lex.read_text (code, Position.file (File.symbolic_path code_path)) @ + ML_Lex.read_text (driver, Position.file (File.symbolic_path driver_path)) @ ML_Lex.read "main ()") handle ERROR msg => error ("Evaluation for " ^ polymlN ^ " failed:\n" ^ msg) in File.read out_path end @@ -503,7 +503,7 @@ case (false, Some(t)) => "False" + t(()) + "\n" }).mkString isabelle.File.write( - isabelle.Path.explode(\ ^ quote (Path.implode (Path.expand out_path)) ^ \<^verbatim>\), + isabelle.Path.explode(\ ^ quote (File.standard_path out_path) ^ \<^verbatim>\), \ ^ quote start_marker ^ \<^verbatim>\ + result_text + \ ^ quote end_marker ^ \<^verbatim>\) }\ val _ = File.write code_path code diff -r b3c5bc06f5be -r 7fd3e461d3b6 src/HOL/Matrix_LP/Cplex_tools.ML --- a/src/HOL/Matrix_LP/Cplex_tools.ML Tue Jan 03 18:23:52 2023 +0100 +++ b/src/HOL/Matrix_LP/Cplex_tools.ML Tue Jan 03 21:22:24 2023 +0100 @@ -1136,7 +1136,7 @@ exception Execute of string; -fun tmp_file s = Path.implode (Path.expand (File.tmp_path (Path.basic s))); +fun tmp_file s = File.standard_path (File.tmp_path (Path.basic s)); fun wrap s = "\""^s^"\""; fun solve_glpk prog = diff -r b3c5bc06f5be -r 7fd3e461d3b6 src/Pure/Admin/afp.scala --- a/src/Pure/Admin/afp.scala Tue Jan 03 18:23:52 2023 +0100 +++ b/src/Pure/Admin/afp.scala Tue Jan 03 21:22:24 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 b3c5bc06f5be -r 7fd3e461d3b6 src/Pure/Admin/build_release.scala --- a/src/Pure/Admin/build_release.scala Tue Jan 03 18:23:52 2023 +0100 +++ b/src/Pure/Admin/build_release.scala Tue Jan 03 21:22:24 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 b3c5bc06f5be -r 7fd3e461d3b6 src/Pure/Admin/check_sources.scala --- a/src/Pure/Admin/check_sources.scala Tue Jan 03 18:23:52 2023 +0100 +++ b/src/Pure/Admin/check_sources.scala Tue Jan 03 21:22:24 2023 +0100 @@ -10,7 +10,7 @@ object Check_Sources { def check_file(path: Path): Unit = { val file_name = path.implode - val file_pos = Position.File(path.implode_symbolic) + val file_pos = Position.File(File.symbolic_path(path)) def line_pos(i: Int) = Position.Line_File(i + 1, file_name) if (space_explode('/', Word.lowercase(path.expand.drop_ext.implode)).contains("aux")) diff -r b3c5bc06f5be -r 7fd3e461d3b6 src/Pure/Admin/jenkins.scala --- a/src/Pure/Admin/jenkins.scala Tue Jan 03 18:23:52 2023 +0100 +++ b/src/Pure/Admin/jenkins.scala Tue Jan 03 21:22:24 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 b3c5bc06f5be -r 7fd3e461d3b6 src/Pure/General/file.ML --- a/src/Pure/General/file.ML Tue Jan 03 18:23:52 2023 +0100 +++ b/src/Pure/General/file.ML Tue Jan 03 21:22:24 2023 +0100 @@ -11,6 +11,7 @@ val bash_path: Path.T -> string val bash_paths: Path.T list -> string val bash_platform_path: Path.T -> string + val symbolic_path: Path.T -> string val absolute_path: Path.T -> Path.T val full_path: Path.T -> Path.T -> Path.T val tmp_path: Path.T -> Path.T @@ -45,6 +46,28 @@ val bash_platform_path = Bash.string o platform_path; +(* symbolic path representation, e.g. "~~/src/Pure/ROOT.ML" *) + +fun symbolic_path path = + let + val directories = rev (space_explode ":" (getenv "ISABELLE_DIRECTORIES")); + val full_name = standard_path path; + fun fold_path a = + (case try (standard_path o Path.explode) a of + SOME b => + if full_name = b then SOME a + else + (case try (unprefix (b ^ "/")) full_name of + SOME name => SOME (a ^ "/" ^ name) + | NONE => NONE) + | NONE => NONE); + in + (case get_first fold_path directories of + SOME name => name + | NONE => Path.implode path) + end; + + (* full_path *) val absolute_path = diff -r b3c5bc06f5be -r 7fd3e461d3b6 src/Pure/General/file.scala --- a/src/Pure/General/file.scala Tue Jan 03 18:23:52 2023 +0100 +++ b/src/Pure/General/file.scala Tue Jan 03 21:22:24 2023 +0100 @@ -52,6 +52,26 @@ def platform_file(path: Path): JFile = new JFile(platform_path(path)) + /* symbolic path representation, e.g. "~~/src/Pure/ROOT.ML" */ + + def symbolic_path(path: Path): String = { + val directories = + Library.space_explode(':', Isabelle_System.getenv("ISABELLE_DIRECTORIES")).reverse + val full_name = standard_path(path) + directories.view.flatMap(a => + try { + val b = standard_path(Path.explode(a)) + if (full_name == b) Some(a) + else { + Library.try_unprefix(b + "/", full_name) match { + case Some(name) => Some(a + "/" + name) + case None => None + } + } + } catch { case ERROR(_) => None }).headOption.getOrElse(path.implode) + } + + /* platform files */ def absolute(file: JFile): JFile = file.toPath.toAbsolutePath.normalize.toFile diff -r b3c5bc06f5be -r 7fd3e461d3b6 src/Pure/General/mercurial.scala --- a/src/Pure/General/mercurial.scala Tue Jan 03 18:23:52 2023 +0100 +++ b/src/Pure/General/mercurial.scala Tue Jan 03 21:22:24 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 b3c5bc06f5be -r 7fd3e461d3b6 src/Pure/General/path.ML --- a/src/Pure/General/path.ML Tue Jan 03 18:23:52 2023 +0100 +++ b/src/Pure/General/path.ML Tue Jan 03 21:22:24 2023 +0100 @@ -37,8 +37,6 @@ val exe: T -> T val expand: T -> T val file_name: T -> string - val implode_symbolic: T -> string - val position: T -> Position.T eqtype binding val binding: T * Position.T -> binding val binding0: T -> binding @@ -238,30 +236,6 @@ val file_name = implode_path o base o expand; -(* implode wrt. given directories *) - -fun implode_symbolic path = - let - val directories = rev (space_explode ":" (getenv "ISABELLE_DIRECTORIES")); - val full_name = implode_path (expand path); - fun fold_path a = - (case try (implode_path o expand o explode_path) a of - SOME b => - if full_name = b then SOME a - else - (case try (unprefix (b ^ "/")) full_name of - SOME name => SOME (a ^ "/" ^ name) - | NONE => NONE) - | NONE => NONE); - in - (case get_first fold_path directories of - SOME name => name - | NONE => implode_path path) - end; - -val position = Position.file o implode_symbolic; - - (* binding: strictly monotonic path with position *) datatype binding = Binding of T * Position.T; diff -r b3c5bc06f5be -r 7fd3e461d3b6 src/Pure/General/path.scala --- a/src/Pure/General/path.scala Tue Jan 03 18:23:52 2023 +0100 +++ b/src/Pure/General/path.scala Tue Jan 03 21:22:24 2023 +0100 @@ -293,26 +293,6 @@ def file_name: String = expand.base.implode - /* implode wrt. given directories */ - - def implode_symbolic: String = { - val directories = - Library.space_explode(':', Isabelle_System.getenv("ISABELLE_DIRECTORIES")).reverse - val full_name = expand.implode - directories.view.flatMap(a => - try { - val b = Path.explode(a).expand.implode - if (full_name == b) Some(a) - else { - Library.try_unprefix(b + "/", full_name) match { - case Some(name) => Some(a + "/" + name) - case None => None - } - } - } catch { case ERROR(_) => None }).headOption.getOrElse(implode) - } - - /* platform files */ def file: JFile = File.platform_file(this) diff -r b3c5bc06f5be -r 7fd3e461d3b6 src/Pure/ML/ml_context.ML --- a/src/Pure/ML/ml_context.ML Tue Jan 03 18:23:52 2023 +0100 +++ b/src/Pure/ML/ml_context.ML Tue Jan 03 21:22:24 2023 +0100 @@ -205,7 +205,7 @@ (* derived versions *) fun eval_file flags path = - let val pos = Path.position path + let val pos = Position.file (File.symbolic_path path) in eval flags pos (ML_Lex.read_text (File.read path, pos)) end; fun eval_source flags source = diff -r b3c5bc06f5be -r 7fd3e461d3b6 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Tue Jan 03 18:23:52 2023 +0100 +++ b/src/Pure/PIDE/command.scala Tue Jan 03 21:22:24 2023 +0100 @@ -471,26 +471,6 @@ Blobs_Info(blobs, index = loaded_files.index) } } - - def build_blobs_info( - syntax: Outer_Syntax, - node_name: Document.Node.Name, - load_commands: List[Command_Span.Span] - ): Blobs_Info = { - val blobs = - for { - span <- load_commands - file <- span.loaded_files(syntax).files - } yield { - (Exn.capture { - val dir = node_name.master_dir_path - val src_path = Path.explode(file) - val name = Document.Node.Name((dir + src_path).expand.implode_symbolic) - Blob.read_file(name, src_path) - }).user_error - } - Blobs_Info(blobs) - } } diff -r b3c5bc06f5be -r 7fd3e461d3b6 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Tue Jan 03 18:23:52 2023 +0100 +++ b/src/Pure/PIDE/document.scala Tue Jan 03 21:22:24 2023 +0100 @@ -120,7 +120,6 @@ def path: Path = Path.explode(File.standard_path(node)) def master_dir: String = Url.strip_base_name(node).getOrElse("") - def master_dir_path: Path = Path.explode(File.standard_path(master_dir)) def is_theory: Boolean = theory.nonEmpty diff -r b3c5bc06f5be -r 7fd3e461d3b6 src/Pure/PIDE/headless.scala --- a/src/Pure/PIDE/headless.scala Tue Jan 03 18:23:52 2023 +0100 +++ b/src/Pure/PIDE/headless.scala Tue Jan 03 21:22:24 2023 +0100 @@ -304,9 +304,7 @@ } val dep_theories = dependencies.theories val dep_theories_set = dep_theories.toSet - val dep_files = - for (path <- dependencies.loaded_files) - yield Document.Node.Name(resources.append_path("", path)) + val dep_files = dependencies.loaded_files val use_theories_state = { val dep_graph = dependencies.theory_graph diff -r b3c5bc06f5be -r 7fd3e461d3b6 src/Pure/PIDE/resources.ML --- a/src/Pure/PIDE/resources.ML Tue Jan 03 18:23:52 2023 +0100 +++ b/src/Pure/PIDE/resources.ML Tue Jan 03 21:22:24 2023 +0100 @@ -245,7 +245,7 @@ let val thy = Theory.begin_theory name parents - |> map_files (fn _ => (Path.explode (Path.implode_symbolic master_dir), imports, [])) + |> map_files (fn _ => (Path.explode (File.symbolic_path master_dir), imports, [])) |> Thy_Header.add_keywords keywords; val ctxt = Proof_Context.init_global thy; val _ = List.app (ignore o check_load_command ctxt o #load_command o #2) keywords; @@ -320,7 +320,7 @@ val text = File.read master_file; val {name = (name, pos), imports, keywords} = - Thy_Header.read (Path.position master_file) text; + Thy_Header.read (Position.file (File.symbolic_path master_file)) text; val _ = thy_base_name <> name andalso error ("Bad theory name " ^ quote name ^ @@ -339,7 +339,7 @@ let val path = File.check_file (File.full_path master_dir src_path); val text = File.read path; - val file_pos = Path.position path; + val file_pos = Position.file (File.symbolic_path path); in (text, file_pos) end; fun read_remote () = @@ -374,7 +374,7 @@ val src_paths = make_paths (Path.explode name); val reports = src_paths |> maps (fn src_path => - [(pos, Markup.path (Path.implode_symbolic (master_dir + src_path))), + [(pos, Markup.path (File.symbolic_path (master_dir + src_path))), (pos, Markup.language_path delimited)]); val _ = Position.reports reports; in map (read_file master_dir o rpair pos) src_paths end @@ -433,7 +433,7 @@ | NONE => master_directory (Proof_Context.theory_of ctxt)); val path = dir + Path.explode name handle ERROR msg => err msg; val _ = Path.expand path handle ERROR msg => err msg; - val _ = Context_Position.report ctxt pos (Markup.path (Path.implode_symbolic path)); + val _ = Context_Position.report ctxt pos (Markup.path (File.symbolic_path path)); val _ = check path handle ERROR msg => err msg; in path end; diff -r b3c5bc06f5be -r 7fd3e461d3b6 src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Tue Jan 03 18:23:52 2023 +0100 +++ b/src/Pure/PIDE/resources.scala Tue Jan 03 21:22:24 2023 +0100 @@ -73,7 +73,14 @@ 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) + + def read_dir(dir: String): List[String] = File.read_dir(Path.explode(dir)) + + def list_thys(dir: String): List[String] = { + val entries = try { read_dir(dir) } catch { case ERROR(_) => Nil } + entries.flatMap(Thy_Header.get_thy_name) + } /* source files of Isabelle/ML bootstrap */ @@ -121,21 +128,18 @@ syntax: Outer_Syntax, name: Document.Node.Name, spans: List[Command_Span.Span] - ) : List[Path] = { - val dir = name.master_dir_path - for { span <- spans; file <- span.loaded_files(syntax).files } - yield (dir + Path.explode(file)).expand + ) : List[Document.Node.Name] = { + for (span <- spans; file <- span.loaded_files(syntax).files) + yield Document.Node.Name(append_path(name.master_dir, Path.explode(file))) } - def pure_files(syntax: Outer_Syntax): List[Path] = { - val pure_dir = Path.explode("~~/src/Pure") - for { - (name, theory) <- Thy_Header.ml_roots - path = (pure_dir + Path.explode(name)).expand - node_name = Document.Node.Name(path.implode, theory = theory) - file <- loaded_files(syntax, node_name, load_commands(syntax, node_name)()) - } yield file - } + def pure_files(syntax: Outer_Syntax): List[Document.Node.Name] = + (for { + (file, theory) <- Thy_Header.ml_roots.iterator + node = append_path("~~/src/Pure", Path.explode(file)) + node_name = Document.Node.Name(node, theory = theory) + name <- loaded_files(syntax, node_name, load_commands(syntax, node_name)()).iterator + } yield name).toList def global_theory(theory: String): Boolean = sessions_structure.global_theories.isDefinedAt(theory) @@ -195,13 +199,11 @@ def complete_import_name(context_name: Document.Node.Name, s: String): List[String] = { val context_session = sessions_structure.theory_qualifier(context_name) - val context_dir = - try { Some(context_name.master_dir_path) } - catch { case ERROR(_) => None } + def context_dir(): List[String] = list_thys(context_name.master_dir) + def session_dir(info: Sessions.Info): List[String] = info.dirs.flatMap(Thy_Header.list_thys) (for { - (session, (info, _)) <- sessions_structure.imports_graph.iterator - dir <- (if (session == context_session) context_dir.toList else info.dirs).iterator - theory <- Thy_Header.list_thy_names(dir).iterator + (session, (info, _)) <- sessions_structure.imports_graph.iterator + theory <- (if (session == context_session) context_dir() else session_dir(info)).iterator if Completion.completed(s)(theory) } yield { if (session == context_session || global_theory(theory)) theory @@ -416,7 +418,7 @@ def loaded_files( name: Document.Node.Name, spans: List[Command_Span.Span] - ) : (String, List[Path]) = { + ) : (String, List[Document.Node.Name]) = { val theory = name.theory val syntax = get_syntax(name) val files1 = resources.loaded_files(syntax, name, spans) @@ -424,7 +426,7 @@ (theory, files1 ::: files2) } - def loaded_files: List[Path] = + def loaded_files: List[Document.Node.Name] = for { (name, spans) <- load_commands file <- loaded_files(name, spans)._2 diff -r b3c5bc06f5be -r 7fd3e461d3b6 src/Pure/System/isabelle_tool.ML --- a/src/Pure/System/isabelle_tool.ML Tue Jan 03 18:23:52 2023 +0100 +++ b/src/Pure/System/isabelle_tool.ML Tue Jan 03 21:22:24 2023 +0100 @@ -17,7 +17,7 @@ fun symbolic_file (a, b) = if a = Markup.fileN - then (a, Path.explode b |> Path.implode_symbolic) + then (a, File.symbolic_path (Path.explode b)) else (a, b); fun isabelle_tools () = diff -r b3c5bc06f5be -r 7fd3e461d3b6 src/Pure/Thy/document_build.scala --- a/src/Pure/Thy/document_build.scala Tue Jan 03 18:23:52 2023 +0100 +++ b/src/Pure/Thy/document_build.scala Tue Jan 03 21:22:24 2023 +0100 @@ -138,7 +138,7 @@ sealed case class Document_Latex(name: Document.Node.Name, body: XML.Body) { def content: File.Content_XML = File.content(Path.basic(tex_name(name)), body) - def file_pos: String = name.path.implode_symbolic + def file_pos: String = File.symbolic_path(name.path) def write(latex_output: Latex.Output, dir: Path): Unit = content.output(latex_output.make(_, file_pos = file_pos)).write(dir) } diff -r b3c5bc06f5be -r 7fd3e461d3b6 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Tue Jan 03 18:23:52 2023 +0100 +++ b/src/Pure/Thy/sessions.scala Tue Jan 03 21:22:24 2023 +0100 @@ -89,7 +89,7 @@ session_base.session_sources.foldLeft(Map.empty) { case (sources, (path, digest)) => def err(): Nothing = error("Incoherent digest for source file: " + path) - val name = path.implode_symbolic + val name = File.symbolic_path(path) sources.get(name) match { case Some(source_file) => if (source_file.digest == digest) sources else err() @@ -357,12 +357,18 @@ val theory_load_commands = (for ((name, span) <- load_commands.iterator) yield name.theory -> span).toMap - val loaded_files = - load_commands.map({ case (name, spans) => dependencies.loaded_files(name, spans) }) + val loaded_files: List[(String, List[Path])] = + for ((name, spans) <- load_commands) yield { + val (theory, files) = dependencies.loaded_files(name, spans) + theory -> files.map(file => Path.explode(file.node)) + } + + val document_files = + for ((path1, path2) <- info.document_files) + yield info.dir + path1 + path2 val session_files = - (theory_files ::: loaded_files.flatMap(_._2) ::: - info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand) + (theory_files ::: loaded_files.flatMap(_._2) ::: document_files).map(_.expand) val imported_files = if (inlined_files) dependencies.imported_files else Nil @@ -469,7 +475,7 @@ val bad = (for { name <- proper_session_theories.iterator - path = name.master_dir_path + path = Path.explode(name.master_dir) if !ok(path.canonical_file) path1 = File.relative_path(info.dir.canonical, path).getOrElse(path) } yield (path1, name)).toList @@ -706,7 +712,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 +1456,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 b3c5bc06f5be -r 7fd3e461d3b6 src/Pure/Thy/thy_header.scala --- a/src/Pure/Thy/thy_header.scala Tue Jan 03 18:23:52 2023 +0100 +++ b/src/Pure/Thy/thy_header.scala Tue Jan 03 21:22:24 2023 +0100 @@ -84,11 +84,9 @@ 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 list_thys(dir: Path): List[String] = { + val entries = try { File.read_dir(dir) } catch { case ERROR(_) => Nil } + entries.flatMap(get_thy_name) } def theory_name(s: String): String = diff -r b3c5bc06f5be -r 7fd3e461d3b6 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Tue Jan 03 18:23:52 2023 +0100 +++ b/src/Pure/Thy/thy_info.ML Tue Jan 03 21:22:24 2023 +0100 @@ -326,7 +326,7 @@ Execution.running Document_ID.none exec_id [] orelse raise Fail ("Failed to register execution: " ^ id); - val text_pos = put_id (Path.position thy_path); + val text_pos = put_id (Position.file (File.symbolic_path thy_path)); val text_props = Position.properties_of text_pos; val _ = remove_thy name; diff -r b3c5bc06f5be -r 7fd3e461d3b6 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Tue Jan 03 18:23:52 2023 +0100 +++ b/src/Pure/Tools/build.scala Tue Jan 03 21:22:24 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 b3c5bc06f5be -r 7fd3e461d3b6 src/Pure/Tools/build_job.scala --- a/src/Pure/Tools/build_job.scala Tue Jan 03 18:23:52 2023 +0100 +++ b/src/Pure/Tools/build_job.scala Tue Jan 03 21:22:24 2023 +0100 @@ -30,21 +30,20 @@ (thy_file, blobs_files) <- theory_context.files(permissive = true) } yield { - val master_dir = - Url.strip_base_name(thy_file).getOrElse( - error("Cannot determine theory master directory: " + quote(thy_file))) - val node_name = Document.Node.Name(thy_file, theory = theory_context.theory) - val results = Command.Results.make( for (elem @ XML.Elem(Markup(_, Markup.Serial(i)), _) <- read_xml(Export.MESSAGES)) yield i -> elem) + val master_dir = + Path.explode(Url.strip_base_name(thy_file).getOrElse( + error("Cannot determine theory master directory: " + quote(thy_file)))) + val blobs = blobs_files.map { file => val name = Document.Node.Name(file) val path = Path.explode(file) - val src_path = File.relative_path(node_name.master_dir_path, path).getOrElse(path) + val src_path = File.relative_path(master_dir, path).getOrElse(path) Command.Blob(name, src_path, None) } val blobs_xml = @@ -72,7 +71,8 @@ yield index -> Markup_Tree.from_XML(xml)) val command = - Command.unparsed(thy_source, theory = true, id = id, node_name = node_name, + Command.unparsed(thy_source, theory = true, id = id, + node_name = Document.Node.Name(thy_file, theory = theory_context.theory), blobs_info = blobs_info, results = results, markups = markups) Document.State.init.snippet(command) @@ -275,11 +275,21 @@ new Session(options, resources) { override val cache: Term.Cache = store.cache - override def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info = { - session_background.base.theory_load_commands.get(name.theory) match { + override def build_blobs_info(node_name: Document.Node.Name): Command.Blobs_Info = { + session_background.base.theory_load_commands.get(node_name.theory) match { case Some(spans) => - val syntax = session_background.base.theory_syntax(name) - Command.build_blobs_info(syntax, name, spans) + val syntax = session_background.base.theory_syntax(node_name) + val blobs = + for (span <- spans; file <- span.loaded_files(syntax).files) + yield { + (Exn.capture { + val master_dir = Path.explode(node_name.master_dir) + val src_path = Path.explode(file) + val node = File.symbolic_path(master_dir + src_path) + Command.Blob.read_file(Document.Node.Name(node), src_path) + }).user_error + } + Command.Blobs_Info(blobs) case None => Command.Blobs_Info.none } } @@ -405,7 +415,8 @@ } export_text(Export.FILES, - cat_lines(snapshot.node_files.map(_.path.implode_symbolic)), compress = false) + cat_lines(snapshot.node_files.map(name => File.symbolic_path(name.path))), + compress = false) for (((_, xml), i) <- snapshot.xml_markup_blobs().zipWithIndex) { export_(Export.MARKUP + (i + 1), xml) diff -r b3c5bc06f5be -r 7fd3e461d3b6 src/Pure/Tools/check_keywords.scala --- a/src/Pure/Tools/check_keywords.scala Tue Jan 03 18:23:52 2023 +0100 +++ b/src/Pure/Tools/check_keywords.scala Tue Jan 03 21:22:24 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 b3c5bc06f5be -r 7fd3e461d3b6 src/Pure/Tools/logo.scala --- a/src/Pure/Tools/logo.scala Tue Jan 03 18:23:52 2023 +0100 +++ b/src/Pure/Tools/logo.scala Tue Jan 03 21:22:24 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 b3c5bc06f5be -r 7fd3e461d3b6 src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Tue Jan 03 18:23:52 2023 +0100 +++ b/src/Tools/Code/code_target.ML Tue Jan 03 21:22:24 2023 +0100 @@ -541,7 +541,7 @@ Markup.markup Markup.keyword2 "file" ^ " argument" ^ Position.here pos); val _ = Position.report pos (Markup.language_path delimited); val path = #1 (Path.explode_pos (s, pos)); - val _ = Position.report pos (Markup.path (Path.implode_symbolic path)); + val _ = Position.report pos (Markup.path (File.symbolic_path path)); in (location, (path, pos)) end end; diff -r b3c5bc06f5be -r 7fd3e461d3b6 src/Tools/VSCode/src/build_vscode_extension.scala --- a/src/Tools/VSCode/src/build_vscode_extension.scala Tue Jan 03 18:23:52 2023 +0100 +++ b/src/Tools/VSCode/src/build_vscode_extension.scala Tue Jan 03 21:22:24 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) diff -r b3c5bc06f5be -r 7fd3e461d3b6 src/Tools/VSCode/src/vscode_resources.scala --- a/src/Tools/VSCode/src/vscode_resources.scala Tue Jan 03 18:23:52 2023 +0100 +++ b/src/Tools/VSCode/src/vscode_resources.scala Tue Jan 03 21:22:24 2023 +0100 @@ -110,6 +110,9 @@ else File.absolute_name(new JFile(prefix + JFile.separator + File.platform_path(path))) } + override def read_dir(dir: String): List[String] = + File.read_dir(Path.explode(File.standard_path(dir))) + def get_models(): Iterable[VSCode_Model] = state.value.models.values def get_model(file: JFile): Option[VSCode_Model] = state.value.models.get(file) def get_model(name: Document.Node.Name): Option[VSCode_Model] = get_model(node_file(name)) diff -r b3c5bc06f5be -r 7fd3e461d3b6 src/Tools/jEdit/src/jedit_resources.scala --- a/src/Tools/jEdit/src/jedit_resources.scala Tue Jan 03 18:23:52 2023 +0100 +++ b/src/Tools/jEdit/src/jedit_resources.scala Tue Jan 03 21:22:24 2023 +0100 @@ -66,6 +66,12 @@ } } + override def read_dir(dir: String): List[String] = { + val vfs = VFSManager.getVFSForPath(dir) + if (vfs.isInstanceOf[FileVFS]) File.read_dir(Path.explode(File.standard_path(dir))) + else Nil + } + /* file content */