--- a/src/Pure/name.ML Thu May 01 09:30:35 2014 +0200
+++ b/src/Pure/name.ML Thu May 01 09:30:36 2014 +0200
@@ -31,6 +31,7 @@
val invent_list: string list -> string -> int -> string list
val variant: string -> context -> string * context
val variant_list: string list -> string list -> string list
+ val enforce_case: bool -> string -> string
val desymbolize: bool option -> string -> string
end;
@@ -150,6 +151,13 @@
(* names conforming to typical requirements of identifiers in the world outside *)
+fun enforce_case' false cs =
+ (if forall Symbol.is_ascii_upper cs then map else nth_map 0) Symbol.to_ascii_lower cs
+ | enforce_case' true cs =
+ nth_map 0 Symbol.to_ascii_upper cs;
+
+fun enforce_case upper = implode o enforce_case' upper o raw_explode;
+
fun desymbolize perhaps_upper "" =
if the_default false perhaps_upper then "X" else "x"
| desymbolize perhaps_upper s =
@@ -171,13 +179,7 @@
(case Symbol.decode x of
Symbol.Sym name => "_" :: raw_explode name @ sep xs
| _ => sep xs);
- fun upper_lower cs =
- case perhaps_upper of
- NONE => cs
- | SOME true => nth_map 0 Symbol.to_ascii_upper cs
- | SOME false =>
- (if forall Symbol.is_ascii_upper cs then map else nth_map 0)
- Symbol.to_ascii_lower cs;
+ val upper_lower = Option.map enforce_case' perhaps_upper |> the_default I;
in fold_rev desymb ys [] |> desep |> upper_lower |> implode end;
end;