# HG changeset patch
# User Lars Hupel <lars.hupel@mytum.de>
# Date 1681592521 -7200
# Node ID 21bb32a7fd58297b6b12f40c3b81373021e5e112
# Parent  a11e25bdd247d96a8dfe7a93d06201e918dcee50# Parent  30389d96d0d68894c974e00b5bad79ab0e583f49
merged

diff -r a11e25bdd247 -r 21bb32a7fd58 src/Pure/General/long_name.ML
--- a/src/Pure/General/long_name.ML	Tue Apr 04 16:06:12 2023 +0200
+++ b/src/Pure/General/long_name.ML	Sat Apr 15 23:02:01 2023 +0200
@@ -7,7 +7,13 @@
 signature LONG_NAME =
 sig
   val separator: string
+  val append: string -> string -> string
+  val qualify: string -> string -> string
   val is_qualified: string -> bool
+  val qualifier: string -> string
+  val base_name: string -> string
+  val map_base_name: (string -> string) -> string -> string
+  val count: string -> int
   val hidden: string -> string
   val is_hidden: string -> bool
   val dest_hidden: string -> string option
@@ -15,17 +21,11 @@
   val dest_local: string -> string option
   val implode: string list -> string
   val explode: string -> string list
-  val append: string -> string -> string
-  val qualification: string -> int
-  val qualify: string -> string -> string
-  val qualifier: string -> string
-  val base_name: string -> string
-  val map_base_name: (string -> string) -> string -> string
   type chunks
   val count_chunks: chunks -> int
   val size_chunks: chunks -> int
   val empty_chunks: chunks
-  val make_chunks: bool list -> string -> chunks
+  val make_chunks: int -> bool list -> string -> chunks
   val chunks: string -> chunks
   val explode_chunks: chunks -> string list
   val implode_chunks: chunks -> string
@@ -42,7 +42,36 @@
 val separator = ".";
 val separator_char = String.nth separator 0;
 
-fun is_qualified name = String.member name separator_char;
+fun append name1 "" = name1
+  | append "" name2 = name2
+  | append name1 name2 = name1 ^ separator ^ name2;
+
+fun qualify qual name =
+  if qual = "" orelse name = "" then name
+  else qual ^ separator ^ name;
+
+fun last_separator name =
+  let fun last i = if i < 0 orelse String.nth name i = separator_char then i else last (i - 1)
+  in last (size name - 1) end;
+
+fun is_qualified name = last_separator name >= 0;
+
+fun qualifier name =
+  let val i = last_separator name
+  in if i < 0 then "" else String.substring (name, 0, i) end;
+
+fun base_name name =
+  let
+    val i = last_separator name;
+    val j = i + 1;
+  in if i < 0 then name else String.substring (name, j, size name - j) end;
+
+fun map_base_name f name =
+  if name = "" then ""
+  else qualify (qualifier name) (f (base_name name));
+
+fun count "" = 0
+  | count name = String.fold (fn c => c = separator_char ? Integer.add 1) name 1;
 
 val hidden_prefix = "??."
 val hidden = prefix hidden_prefix;
@@ -55,22 +84,6 @@
 val implode = space_implode separator;
 val explode = space_explode separator;
 
-fun append name1 "" = name1
-  | append "" name2 = name2
-  | append name1 name2 = name1 ^ separator ^ name2;
-
-fun qualification "" = 0
-  | qualification name = fold_string (fn s => s = separator ? Integer.add 1) name 1;
-
-fun qualify qual name =
-  if qual = "" orelse name = "" then name
-  else qual ^ separator ^ name;
-
-fun map_base_name _ "" = ""
-  | map_base_name f name =
-      let val names = explode name
-      in implode (nth_map (length names - 1) f names) end;
-
 
 (* compact representation of chunks *)
 
@@ -100,18 +113,31 @@
 
 val empty_chunks = Chunks {count = 0, size = 0, mask = 0w0, string = ""};
 
-fun make_chunks suppress string =
+fun make_chunks suppress1 suppress2 string =
   let
     val {string_end, chunk_end, ...} = string_ops string;
 
     fun err msg = raise Fail ("Malformed qualified name " ^ quote string ^ ":\n  " ^ msg);
 
-    fun make suppr i k l m s =
+    fun make suppr1 suppr2 i k l m s =
       let
         val is_end = chunk_end i;
-        val keep = null suppr orelse not (hd suppr);
 
-        val suppr' = if is_end andalso not (null suppr) then tl suppr else suppr;
+        val suppr =
+          if suppr1 > 0 then true
+          else if suppr1 < 0 then false
+          else if null suppr2 then false
+          else hd suppr2;
+        val suppr1' =
+          if is_end andalso suppr1 > 0 then suppr1 - 1
+          else if is_end andalso suppr1 < 0 then suppr1 + 1
+          else suppr1;
+        val suppr2' =
+          if is_end andalso suppr1 = 0 andalso not (null suppr2)
+          then tl suppr2 else suppr2;
+
+        val keep = not suppr;
+
         val l' = if keep then l + 1 else l;
         val k' = if is_end andalso keep andalso l' > 0 then k + 1 else k;
         val m' =
@@ -121,14 +147,15 @@
           else mask_set s m;
         val s' = if is_end then mask_push s else s;
       in
-        if not (string_end i) then make suppr' (i + 1) k' l' m' s'
-        else if not (null suppr') then err ("cannot suppress chunks beyond " ^ string_of_int k')
+        if not (string_end i) then make suppr1' suppr2' (i + 1) k' l' m' s'
+        else if not (suppr1' = 0 andalso null suppr2') then
+          err ("cannot suppress chunks beyond " ^ string_of_int k')
         else if k' = 0 then empty_chunks
         else Chunks {count = k', size = Int.max (0, l' - 1), mask = m', string = string}
       end;
-  in make suppress 0 0 0 0w0 0w1 end;
+  in make suppress1 suppress2 0 0 0 0w0 0w1 end;
 
-val chunks = make_chunks [];
+val chunks = make_chunks 0 [];
 
 fun expand_chunks f (Chunks {count, size, mask, string}) =
   let
@@ -179,17 +206,4 @@
 
 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;
diff -r a11e25bdd247 -r 21bb32a7fd58 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Tue Apr 04 16:06:12 2023 +0200
+++ b/src/Pure/General/name_space.ML	Sat Apr 15 23:02:01 2023 +0200
@@ -283,7 +283,7 @@
           EQUAL =>
             (case bool_ord (apply2 (is_some o Long_Name.dest_local) (name2, name1)) of
               EQUAL =>
-                (case int_ord (apply2 Long_Name.qualification (xname1, xname2)) of
+                (case int_ord (apply2 Long_Name.count (xname1, xname2)) of
                   EQUAL => string_ord (xname1, xname2)
                 | ord => ord)
             | ord => ord)
diff -r a11e25bdd247 -r 21bb32a7fd58 src/Pure/General/vector.ML
--- a/src/Pure/General/vector.ML	Tue Apr 04 16:06:12 2023 +0200
+++ b/src/Pure/General/vector.ML	Sat Apr 15 23:02:01 2023 +0200
@@ -9,6 +9,7 @@
   include VECTOR
   val nth: 'a vector -> int -> 'a
   val forall: ('a -> bool) -> 'a vector -> bool
+  val member: ('a * 'a -> bool) -> 'a vector -> 'a -> bool
   val fold: ('a -> 'b -> 'b) -> 'a vector -> 'b -> 'b
   val fold_rev: ('a -> 'b -> 'b) -> 'a vector -> 'b -> 'b
 end;
@@ -22,6 +23,8 @@
 
 val forall = all;
 
+fun member eq vec x = exists (fn y => eq (x, y)) vec;
+
 fun fold f vec x = foldl (fn (a, b) => f a b) x vec;
 fun fold_rev f vec x = foldr (fn (a, b) => f a b) x vec;
 
diff -r a11e25bdd247 -r 21bb32a7fd58 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Tue Apr 04 16:06:12 2023 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Sat Apr 15 23:02:01 2023 +0200
@@ -335,7 +335,7 @@
 
 val index_ord = option_ord (K EQUAL);
 val hidden_ord = bool_ord o apply2 Long_Name.is_hidden;
-val qual_ord = int_ord o apply2 Long_Name.qualification;
+val qual_ord = int_ord o apply2 Long_Name.count;
 val txt_ord = int_ord o apply2 size;
 
 fun nicer_name ((a, x), i) ((b, y), j) =