--- a/src/Tools/Code/code_namespace.ML Thu Oct 02 22:33:45 2014 +0200
+++ b/src/Tools/Code/code_namespace.ML Thu Oct 02 17:51:04 2014 +0200
@@ -6,6 +6,8 @@
signature CODE_NAMESPACE =
sig
+ val variant_case_insensitive: string -> Name.context -> string * Name.context
+
datatype export = Private | Opaque | Public
val is_public: export -> bool
val not_private: export -> bool
@@ -47,6 +49,25 @@
structure Code_Namespace : CODE_NAMESPACE =
struct
+(** name handling on case-insensitive file systems **)
+
+fun restore_for cs =
+ if forall Symbol.is_ascii_upper cs then map Symbol.to_ascii_upper
+ else if Symbol.is_ascii_upper (nth cs 0) then nth_map 0 Symbol.to_ascii_upper
+ else I;
+
+fun variant_case_insensitive s ctxt =
+ let
+ val cs = Symbol.explode s;
+ val s_lower = implode (map Symbol.to_ascii_lower cs);
+ val restore = implode o restore_for cs o Symbol.explode;
+ in
+ ctxt
+ |> Name.variant s_lower
+ |>> restore
+ end;
+
+
(** export **)
datatype export = Private | Opaque | Public;