--- 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
--- 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;