# HG changeset patch
# User wenzelm
# Date 1682516329 -7200
# Node ID 019186a60c84cb24be11347ae405f3203a098e46
# Parent  430e6c477ba4986e9943625218c8dba52b813af6
tuned signature;

diff -r 430e6c477ba4 -r 019186a60c84 src/Pure/General/long_name.ML
--- a/src/Pure/General/long_name.ML	Sun Apr 23 21:31:00 2023 +0200
+++ b/src/Pure/General/long_name.ML	Wed Apr 26 15:38:49 2023 +0200
@@ -26,8 +26,8 @@
   val size_chunks: chunks -> int
   val empty_chunks: chunks
   val base_chunks: string -> chunks
-  val make_chunks: int -> bool list -> string -> chunks
-  val chunks: string -> chunks
+  val suppress_chunks: int -> bool list -> string -> chunks
+  val make_chunks: string -> chunks
   val explode_chunks: chunks -> string list
   val implode_chunks: chunks -> string
   val compare_chunks: chunks * chunks -> order
@@ -114,13 +114,13 @@
 
 val empty_chunks = Chunks {count = 0, size = 0, mask = 0w0, string = ""};
 
-fun make_chunks suppress1 suppress2 string =
+fun suppress_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 suppr1 suppr2 i k l m s =
+    fun suppr_chunks suppr1 suppr2 i k l m s =
       let
         val is_end = chunk_end i;
 
@@ -148,18 +148,18 @@
           else mask_set s m;
         val s' = if is_end then mask_push s else s;
       in
-        if not (string_end i) then make suppr1' suppr2' (i + 1) k' l' m' s'
+        if not (string_end i) then suppr_chunks 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 suppress1 suppress2 0 0 0 0w0 0w1 end;
+  in suppr_chunks suppress1 suppress2 0 0 0 0w0 0w1 end;
 
-val chunks = make_chunks 0 [];
+val make_chunks = suppress_chunks 0 [];
 
 fun base_chunks name =
-  make_chunks (Int.max (0, count name - 1)) [] name;
+  suppress_chunks (Int.max (0, count name - 1)) [] name;
 
 fun expand_chunks f (Chunks {count, size, mask, string}) =
   let
diff -r 430e6c477ba4 -r 019186a60c84 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Sun Apr 23 21:31:00 2023 +0200
+++ b/src/Pure/General/name_space.ML	Wed Apr 26 15:38:49 2023 +0200
@@ -136,7 +136,7 @@
 fun del_name_extra name =
   map_internals (apfst (fn [] => [] | x :: xs => x :: remove (op =) name xs));
 val add_name = map_internals o apfst o update (op =);
-fun hide_name name = map_internals (apsnd (update (op =) name)) (Long_Name.chunks name);
+fun hide_name name = map_internals (apsnd (update (op =) name)) (Long_Name.make_chunks name);
 
 
 (* external accesses *)
@@ -221,7 +221,7 @@
   | ([], []) => (Long_Name.hidden (Long_Name.implode_chunks xname), true)
   | ([], name' :: _) => (Long_Name.hidden name', true));
 
-fun intern space = #1 o intern_chunks space o Long_Name.chunks;
+fun intern space = #1 o intern_chunks space o Long_Name.make_chunks;
 
 fun is_valid_access space name xname =
   (case lookup_internals space xname of
@@ -246,7 +246,7 @@
       in name = name' andalso (not require_unique orelse is_unique) end;
 
     fun extern [] =
-          if valid false (Long_Name.chunks name) then name
+          if valid false (Long_Name.make_chunks name) then name
           else Long_Name.hidden name
       | extern (a :: bs) =
           if valid names_unique a then Long_Name.implode_chunks a
@@ -472,7 +472,7 @@
           val sfxs = restrict (mandatory_suffixes spec);
           val pfxs = restrict (mandatory_prefixes spec);
         in apply2 (map Long_Name.implode o distinct op =) (sfxs @ pfxs, sfxs) end;
-  in (apply2 (map Long_Name.chunks) accesses (* FIXME proper make_chunks mask*), args) end;
+  in (apply2 (map Long_Name.make_chunks) accesses (* FIXME suppress_chunks *), args) end;
 
 end;