--- a/src/HOL/Library/code_test.ML Tue Jan 03 15:42:25 2023 +0100
+++ b/src/HOL/Library/code_test.ML Tue Jan 03 16:05:07 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, Position.file (Path.implode_symbolic code_path)) @
- ML_Lex.read_text (driver, Position.file (Path.implode_symbolic 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
--- a/src/Pure/Admin/check_sources.scala Tue Jan 03 15:42:25 2023 +0100
+++ b/src/Pure/Admin/check_sources.scala Tue Jan 03 16:05:07 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/General/file.ML Tue Jan 03 15:42:25 2023 +0100
+++ b/src/Pure/General/file.ML Tue Jan 03 16:05:07 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 15:42:25 2023 +0100
+++ b/src/Pure/General/file.scala Tue Jan 03 16:05:07 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/path.ML Tue Jan 03 15:42:25 2023 +0100
+++ b/src/Pure/General/path.ML Tue Jan 03 16:05:07 2023 +0100
@@ -37,7 +37,6 @@
val exe: T -> T
val expand: T -> T
val file_name: T -> string
- val implode_symbolic: T -> string
eqtype binding
val binding: T * Position.T -> binding
val binding0: T -> binding
@@ -237,28 +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;
-
-
(* binding: strictly monotonic path with position *)
datatype binding = Binding of T * Position.T;
--- a/src/Pure/General/path.scala Tue Jan 03 15:42:25 2023 +0100
+++ b/src/Pure/General/path.scala Tue Jan 03 16:05:07 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 15:42:25 2023 +0100
+++ b/src/Pure/ML/ml_context.ML Tue Jan 03 16:05:07 2023 +0100
@@ -205,7 +205,7 @@
(* derived versions *)
fun eval_file flags path =
- let val pos = Position.file (Path.implode_symbolic 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/resources.ML Tue Jan 03 15:42:25 2023 +0100
+++ b/src/Pure/PIDE/resources.ML Tue Jan 03 16:05:07 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 (Position.file (Path.implode_symbolic 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 = Position.file (Path.implode_symbolic 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/System/isabelle_tool.ML Tue Jan 03 15:42:25 2023 +0100
+++ b/src/Pure/System/isabelle_tool.ML Tue Jan 03 16:05:07 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 15:42:25 2023 +0100
+++ b/src/Pure/Thy/document_build.scala Tue Jan 03 16:05:07 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 15:42:25 2023 +0100
+++ b/src/Pure/Thy/sessions.scala Tue Jan 03 16:05:07 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()
--- a/src/Pure/Thy/thy_info.ML Tue Jan 03 15:42:25 2023 +0100
+++ b/src/Pure/Thy/thy_info.ML Tue Jan 03 16:05:07 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 (Position.file (Path.implode_symbolic 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_job.scala Tue Jan 03 15:42:25 2023 +0100
+++ b/src/Pure/Tools/build_job.scala Tue Jan 03 16:05:07 2023 +0100
@@ -285,7 +285,7 @@
(Exn.capture {
val master_dir = Path.explode(node_name.master_dir)
val src_path = Path.explode(file)
- val node = (master_dir + src_path).expand.implode_symbolic
+ val node = File.symbolic_path(master_dir + src_path)
Command.Blob.read_file(Document.Node.Name(node), src_path)
}).user_error
}
@@ -415,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/Tools/Code/code_target.ML Tue Jan 03 15:42:25 2023 +0100
+++ b/src/Tools/Code/code_target.ML Tue Jan 03 16:05:07 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;