--- a/src/Pure/name.ML Thu May 01 09:30:34 2014 +0200
+++ b/src/Pure/name.ML Thu May 01 09:30:35 2014 +0200
@@ -31,7 +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 desymbolize: bool -> string -> string
+ val desymbolize: bool option -> string -> string
end;
structure Name: NAME =
@@ -150,8 +150,9 @@
(* names conforming to typical requirements of identifiers in the world outside *)
-fun desymbolize upper "" = if upper then "X" else "x"
- | desymbolize upper s =
+fun desymbolize perhaps_upper "" =
+ if the_default false perhaps_upper then "X" else "x"
+ | desymbolize perhaps_upper s =
let
val xs as (x :: _) = Symbol.explode s;
val ys =
@@ -171,10 +172,12 @@
Symbol.Sym name => "_" :: raw_explode name @ sep xs
| _ => sep xs);
fun upper_lower cs =
- if upper then nth_map 0 Symbol.to_ascii_upper cs
- else
- (if forall Symbol.is_ascii_upper cs then map else nth_map 0)
- Symbol.to_ascii_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;
in fold_rev desymb ys [] |> desep |> upper_lower |> implode end;
end;