src/Tools/Code/code_namespace.ML
changeset 58520 a4d1f8041af0
parent 57428 47c8475e7864
child 59058 a78612c67ec0
     1.1 --- a/src/Tools/Code/code_namespace.ML	Thu Oct 02 22:33:45 2014 +0200
     1.2 +++ b/src/Tools/Code/code_namespace.ML	Thu Oct 02 17:51:04 2014 +0200
     1.3 @@ -6,6 +6,8 @@
     1.4  
     1.5  signature CODE_NAMESPACE =
     1.6  sig
     1.7 +  val variant_case_insensitive: string -> Name.context -> string * Name.context
     1.8 +
     1.9    datatype export = Private | Opaque | Public
    1.10    val is_public: export -> bool
    1.11    val not_private: export -> bool
    1.12 @@ -47,6 +49,25 @@
    1.13  structure Code_Namespace : CODE_NAMESPACE =
    1.14  struct
    1.15  
    1.16 +(** name handling on case-insensitive file systems **)
    1.17 +
    1.18 +fun restore_for cs =
    1.19 +  if forall Symbol.is_ascii_upper cs then map Symbol.to_ascii_upper
    1.20 +  else if Symbol.is_ascii_upper (nth cs 0) then nth_map 0 Symbol.to_ascii_upper
    1.21 +  else I;
    1.22 +
    1.23 +fun variant_case_insensitive s ctxt =
    1.24 +  let
    1.25 +    val cs = Symbol.explode s;
    1.26 +    val s_lower = implode (map Symbol.to_ascii_lower cs);
    1.27 +    val restore = implode o restore_for cs o Symbol.explode;
    1.28 +  in
    1.29 +    ctxt
    1.30 +    |> Name.variant s_lower
    1.31 +    |>> restore
    1.32 +  end;
    1.33 +
    1.34 +
    1.35  (** export **)
    1.36  
    1.37  datatype export = Private | Opaque | Public;