# HG changeset patch
# User wenzelm
# Date 1672750859 -3600
# Node ID 6a07cf09604d70df06f46f9fb007944ae47591db
# Parent  cccd1a583c8180a35c34340853ba0ff08f138e3e
tuned signature: avoid too many aliases (see also 72daee8a39ca);

diff -r cccd1a583c81 -r 6a07cf09604d src/HOL/Library/code_test.ML
--- a/src/HOL/Library/code_test.ML	Tue Jan 03 12:58:00 2023 +0100
+++ b/src/HOL/Library/code_test.ML	Tue Jan 03 14:00:59 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 (Path.implode_symbolic code_path)) @
+         ML_Lex.read_text (driver, Position.file (Path.implode_symbolic driver_path)) @
          ML_Lex.read "main ()")
       handle ERROR msg => error ("Evaluation for " ^ polymlN ^ " failed:\n" ^ msg)
   in File.read out_path end
diff -r cccd1a583c81 -r 6a07cf09604d src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Tue Jan 03 12:58:00 2023 +0100
+++ b/src/Pure/General/path.ML	Tue Jan 03 14:00:59 2023 +0100
@@ -38,7 +38,6 @@
   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
@@ -259,8 +258,6 @@
     | NONE => implode_path path)
   end;
 
-val position = Position.file o implode_symbolic;
-
 
 (* binding: strictly monotonic path with position *)
 
diff -r cccd1a583c81 -r 6a07cf09604d src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Tue Jan 03 12:58:00 2023 +0100
+++ b/src/Pure/ML/ml_context.ML	Tue Jan 03 14:00:59 2023 +0100
@@ -205,7 +205,7 @@
 (* derived versions *)
 
 fun eval_file flags path =
-  let val pos = Path.position path
+  let val pos = Position.file (Path.implode_symbolic path)
   in eval flags pos (ML_Lex.read_text (File.read path, pos)) end;
 
 fun eval_source flags source =
diff -r cccd1a583c81 -r 6a07cf09604d src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Tue Jan 03 12:58:00 2023 +0100
+++ b/src/Pure/PIDE/resources.ML	Tue Jan 03 14:00:59 2023 +0100
@@ -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 (Path.implode_symbolic 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 (Path.implode_symbolic path);
       in (text, file_pos) end;
 
     fun read_remote () =
diff -r cccd1a583c81 -r 6a07cf09604d src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Tue Jan 03 12:58:00 2023 +0100
+++ b/src/Pure/Thy/thy_info.ML	Tue Jan 03 14:00:59 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 (Path.implode_symbolic thy_path));
     val text_props = Position.properties_of text_pos;
 
     val _ = remove_thy name;