equal
deleted
inserted
replaced
24 val invents: context -> string -> int -> string list |
24 val invents: context -> string -> int -> string list |
25 val names: context -> string -> 'a list -> (string * 'a) list |
25 val names: context -> string -> 'a list -> (string * 'a) list |
26 val invent_list: string list -> string -> int -> string list |
26 val invent_list: string list -> string -> int -> string list |
27 val variants: string list -> context -> string list * context |
27 val variants: string list -> context -> string list * context |
28 val variant_list: string list -> string list -> string list |
28 val variant_list: string list -> string list -> string list |
29 val variant: string list -> string -> string |
|
30 val desymbolize: bool -> string -> string |
29 val desymbolize: bool -> string -> string |
31 end; |
30 end; |
32 |
31 |
33 structure Name: NAME = |
32 structure Name: NAME = |
34 struct |
33 struct |
135 |> declare x'; |
134 |> declare x'; |
136 in (x', ctxt') end; |
135 in (x', ctxt') end; |
137 in (x' ^ replicate_string n "_", ctxt') end); |
136 in (x' ^ replicate_string n "_", ctxt') end); |
138 |
137 |
139 fun variant_list used names = #1 (make_context used |> variants names); |
138 fun variant_list used names = #1 (make_context used |> variants names); |
140 fun variant used = singleton (variant_list used); |
|
141 |
139 |
142 |
140 |
143 (* names conforming to typical requirements of identifiers in the world outside *) |
141 (* names conforming to typical requirements of identifiers in the world outside *) |
144 |
142 |
145 fun desymbolize upper "" = if upper then "X" else "x" |
143 fun desymbolize upper "" = if upper then "X" else "x" |