--- 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(\<close> ^ quote (Path.implode (Path.expand out_path)) ^ \<^verbatim>\<open>),
+ isabelle.Path.explode(\<close> ^ quote (File.standard_path out_path) ^ \<^verbatim>\<open>),
\<close> ^ quote start_marker ^ \<^verbatim>\<open> + result_text + \<close> ^ quote end_marker ^ \<^verbatim>\<open>)
}\<close>
val _ = File.write code_path code
--- 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 =
--- 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
--- 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
--- 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"))
--- 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 =
--- 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 =
--- 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
--- 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"
--- 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;
--- 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)
--- 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 =
--- 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)
- }
}
--- 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
--- 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
--- 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;
--- 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
--- 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 () =
--- 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)
}
--- 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 */
--- 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 =
--- 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;
--- 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 ", ""))
}
}
--- 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)
--- 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)) =>
--- 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))
}
}
--- 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;
--- 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)
--- 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))
--- 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 */