clarified signature, following Isabelle/Scala;
authorwenzelm
Fri, 17 Jan 2025 11:16:11 +0100
changeset 81842 5900b58d6bd4
parent 81841 c84c0c0e6907
child 81843 4329a8fecbe1
clarified signature, following Isabelle/Scala;
src/Pure/General/path.ML
src/Pure/Tools/generated_files.ML
--- a/src/Pure/General/path.ML	Fri Jan 17 11:05:36 2025 +0100
+++ b/src/Pure/General/path.ML	Fri Jan 17 11:16:11 2025 +0100
@@ -33,7 +33,6 @@
   val ext: string -> T -> T
   val platform_exe: T -> T
   val split_ext: T -> T * string
-  val exe: T -> T
   val expand: T -> T
   val file_name: T -> string
   eqtype binding
@@ -213,8 +212,6 @@
     ([], _) => (Path [Basic s], "")
   | (cs, e) => (Path [Basic (implode (take (length cs - 1) cs))], implode e)));
 
-val exe = ML_System.platform_is_windows ? ext "exe";
-
 
 (* expand variables *)
 
--- a/src/Pure/Tools/generated_files.ML	Fri Jan 17 11:05:36 2025 +0100
+++ b/src/Pure/Tools/generated_files.ML	Fri Jan 17 11:16:11 2025 +0100
@@ -343,7 +343,8 @@
         export |> List.app (fn (bindings, executable) =>
           bindings |> List.app (fn binding0 =>
             let
-              val binding = binding0 |> Path.map_binding (executable = SOME true ? Path.exe);
+              val binding = binding0
+                |> Path.map_binding (executable = SOME true ? Path.platform_exe);
               val (path, pos) = Path.dest_binding binding;
               val content =
                 (case try Bytes.read (dir + path) of