# HG changeset patch
# User wenzelm
# Date 1681422792 -7200
# Node ID f56697bfd67b2e487e840afe4c386b7d15a3f300
# Parent  0eb54e7004eb30d82e580b9de0af9f58d6bfe8fe
minor performance tuning;

diff -r 0eb54e7004eb -r f56697bfd67b src/Pure/General/long_name.ML
--- a/src/Pure/General/long_name.ML	Thu Apr 13 23:16:18 2023 +0200
+++ b/src/Pure/General/long_name.ML	Thu Apr 13 23:53:12 2023 +0200
@@ -66,12 +66,6 @@
   if qual = "" orelse name = "" then name
   else qual ^ separator ^ name;
 
-fun qualifier "" = ""
-  | qualifier name = implode (#1 (split_last (explode name)));
-
-fun base_name "" = ""
-  | base_name name = List.last (explode name);
-
 fun map_base_name _ "" = ""
   | map_base_name f name =
       let val names = explode name
@@ -185,4 +179,17 @@
 
 structure Chunks = Change_Table(type key = chunks val ord = compare_chunks);
 
+
+(* split name *)
+
+fun qualifier name =
+  if is_qualified name
+  then String.substring (name, 0, Int.max (0, List.last (expand_chunks #2 (chunks name)) - 1))
+  else "";
+
+fun base_name name =
+  if is_qualified name
+  then String.substring (List.last (expand_chunks I (chunks name)))
+  else name;
+
 end;