src/Pure/name.ML
changeset 31035 de0a20a030fd
parent 31013 69a476d6fea6
child 33095 bbd52d2f8696
     1.1 --- a/src/Pure/name.ML	Mon May 04 14:49:49 2009 +0200
     1.2 +++ b/src/Pure/name.ML	Mon May 04 14:49:50 2009 +0200
     1.3 @@ -28,7 +28,7 @@
     1.4    val variants: string list -> context -> string list * context
     1.5    val variant_list: string list -> string list -> string list
     1.6    val variant: string list -> string -> string
     1.7 -  val desymbolize: string -> string
     1.8 +  val desymbolize: bool -> string -> string
     1.9  end;
    1.10  
    1.11  structure Name: NAME =
    1.12 @@ -146,25 +146,30 @@
    1.13  fun variant used = singleton (variant_list used);
    1.14  
    1.15  
    1.16 -(* names conforming to typical requirements of identifiers in the outside world *)
    1.17 +(* names conforming to typical requirements of identifiers in the world outside *)
    1.18  
    1.19 -fun desymbolize "" = "x"
    1.20 -  | desymbolize s =
    1.21 +fun desymbolize upper "" = if upper then "X" else "x"
    1.22 +  | desymbolize upper s =
    1.23        let
    1.24 -        val xs = Symbol.explode s;
    1.25 -        val ys = if Symbol.is_ascii_letter (hd xs) then xs
    1.26 +        val xs as (x :: _) = Symbol.explode s;
    1.27 +        val ys = if Symbol.is_ascii_letter x orelse Symbol.is_symbolic x then xs
    1.28            else "x" :: xs;
    1.29          fun is_valid x =
    1.30            Symbol.is_ascii_letter x orelse Symbol.is_ascii_digit x orelse x = "'";
    1.31          fun sep [] = []
    1.32            | sep (xs as "_" :: _) = xs
    1.33            | sep xs = "_" :: xs;
    1.34 +        fun desep ("_" :: xs) = xs
    1.35 +          | desep xs = xs;
    1.36          fun desymb x xs = if is_valid x
    1.37              then x :: xs
    1.38            else if Symbol.is_symbolic x
    1.39 -            then "_" :: Symbol.name_of x :: sep xs 
    1.40 +            then "_" :: explode (Symbol.name_of x) @ sep xs
    1.41            else
    1.42              sep xs
    1.43 -      in implode (fold_rev desymb ys []) end;
    1.44 +        fun upper_lower cs = if upper then nth_map 0 Symbol.to_ascii_upper cs
    1.45 +          else (if forall Symbol.is_ascii_upper cs
    1.46 +            then map else nth_map 0) Symbol.to_ascii_lower cs;
    1.47 +      in fold_rev desymb ys [] |> desep |> upper_lower |> implode end;
    1.48  
    1.49  end;