# HG changeset patch
# User wenzelm
# Date 1737109480 -3600
# Node ID 4329a8fecbe151a203358d36302b478de6fcc9b7
# Parent  5900b58d6bd488102ffa66c315cba9c2c7de8bc9
tuned signature, following Isabelle/Scala;

diff -r 5900b58d6bd4 -r 4329a8fecbe1 src/HOL/SPARK/Tools/spark_commands.ML
--- a/src/HOL/SPARK/Tools/spark_commands.ML	Fri Jan 17 11:16:11 2025 +0100
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Fri Jan 17 11:24:40 2025 +0100
@@ -13,7 +13,7 @@
     val ([{src_path, lines = vc_lines, pos = vc_pos, ...}: Token.file,
       {lines = fdl_lines, pos = fdl_pos, ...},
       {lines = rls_lines, pos = rls_pos, ...}], thy') = files thy;
-    val path = fst (Path.split_ext src_path);
+    val path = Path.drop_ext src_path;
   in
     SPARK_VCs.set_vcs
       (snd (Fdl_Parser.parse_declarations fdl_pos (cat_lines fdl_lines)))
diff -r 5900b58d6bd4 -r 4329a8fecbe1 src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Fri Jan 17 11:16:11 2025 +0100
+++ b/src/Pure/General/path.ML	Fri Jan 17 11:24:40 2025 +0100
@@ -33,6 +33,8 @@
   val ext: string -> T -> T
   val platform_exe: T -> T
   val split_ext: T -> T * string
+  val drop_ext: T -> T
+  val get_ext: T -> string
   val expand: T -> T
   val file_name: T -> string
   eqtype binding
@@ -212,6 +214,9 @@
     ([], _) => (Path [Basic s], "")
   | (cs, e) => (Path [Basic (implode (take (length cs - 1) cs))], implode e)));
 
+val drop_ext = #1 o split_ext;
+val get_ext = #2 o split_ext;
+
 
 (* expand variables *)
 
diff -r 5900b58d6bd4 -r 4329a8fecbe1 src/Pure/Tools/generated_files.ML
--- a/src/Pure/Tools/generated_files.ML	Fri Jan 17 11:16:11 2025 +0100
+++ b/src/Pure/Tools/generated_files.ML	Fri Jan 17 11:24:40 2025 +0100
@@ -253,7 +253,7 @@
 
     val (path, pos) = Path.dest_binding binding;
     val file_type =
-      get_file_type thy (#2 (Path.split_ext path))
+      get_file_type thy (Path.get_ext path)
         handle ERROR msg => error (msg ^ Position.here pos);
 
     val header = #make_comment file_type " generated by Isabelle ";