src/Tools/Code/code_namespace.ML
changeset 56826 ba18bd41e510
parent 55776 7dd1971b39c1
child 57428 47c8475e7864
     1.1 --- a/src/Tools/Code/code_namespace.ML	Fri May 02 14:15:23 2014 +0200
     1.2 +++ b/src/Tools/Code/code_namespace.ML	Fri May 02 21:18:50 2014 +0200
     1.3 @@ -158,13 +158,14 @@
     1.4    then module_fragments' { identifiers = identifiers, reserved = reserved }
     1.5    else K (Long_Name.explode module_name);
     1.6  
     1.7 -fun build_module_namespace ctxt { module_prefix, module_name, identifiers, reserved } program =
     1.8 +fun build_module_namespace ctxt enforce_upper { module_prefix, module_name, identifiers, reserved } program =
     1.9    let
    1.10      val module_names = Code_Symbol.Graph.fold (insert (op =) o Code_Symbol.default_prefix ctxt o fst) program [];
    1.11      val module_fragments' = module_fragments
    1.12        { module_name = module_name, identifiers = identifiers, reserved = reserved };
    1.13 +    val adjust_case = if enforce_upper then map (Name.enforce_case true) else I;
    1.14    in
    1.15 -    fold (fn name => Symtab.update (name, Long_Name.explode module_prefix @ module_fragments' name))
    1.16 +    fold (fn name => Symtab.update (name, adjust_case (Long_Name.explode module_prefix @ module_fragments' name)))
    1.17        module_names Symtab.empty
    1.18    end;
    1.19  
    1.20 @@ -195,7 +196,7 @@
    1.21    let
    1.22  
    1.23      (* building module name hierarchy *)
    1.24 -    val module_namespace = build_module_namespace ctxt { module_prefix = module_prefix,
    1.25 +    val module_namespace = build_module_namespace ctxt true { module_prefix = module_prefix,
    1.26        module_name = module_name, identifiers = identifiers, reserved = reserved } program;
    1.27      val prep_sym = prep_symbol ctxt { module_namespace = module_namespace,
    1.28        force_module = Long_Name.explode module_name, identifiers = identifiers }
    1.29 @@ -317,7 +318,7 @@
    1.30    let
    1.31  
    1.32      (* building module name hierarchy *)
    1.33 -    val module_namespace = build_module_namespace ctxt { module_prefix = "",
    1.34 +    val module_namespace = build_module_namespace ctxt false { module_prefix = "",
    1.35        module_name = module_name, identifiers = identifiers, reserved = reserved } program;
    1.36      val prep_sym = prep_symbol ctxt { module_namespace = module_namespace,
    1.37        force_module = Long_Name.explode module_name, identifiers = identifiers }