explicit module names have precedence over identifier declarations
authorhaftmann
Thu Sep 05 18:05:03 2013 +0200 (2013-09-05)
changeset 53414dd64696d267a
parent 53413 ca3fdc640ebf
child 53425 f5b1f555b73b
explicit module names have precedence over identifier declarations
src/Tools/Code/code_namespace.ML
     1.1 --- a/src/Tools/Code/code_namespace.ML	Thu Sep 05 18:05:02 2013 +0200
     1.2 +++ b/src/Tools/Code/code_namespace.ML	Thu Sep 05 18:05:03 2013 +0200
     1.3 @@ -48,10 +48,11 @@
     1.4    Code_Symbol.lookup identifiers (symbol_of name)
     1.5    |> Option.map (split_last o Long_Name.explode);
     1.6  
     1.7 -fun force_identifier symbol_of fragments_tab identifiers name =
     1.8 +fun force_identifier symbol_of fragments_tab force_module identifiers name =
     1.9    case lookup_identifier symbol_of identifiers name of
    1.10        NONE => (apfst (the o Symtab.lookup fragments_tab) o split_name) name
    1.11 -    | SOME name' => name';
    1.12 +    | SOME prefix_name => if null force_module then prefix_name
    1.13 +        else (force_module, snd prefix_name);
    1.14  
    1.15  fun build_module_namespace { module_prefix, module_identifiers, reserved } program =
    1.16    let
    1.17 @@ -79,7 +80,7 @@
    1.18        else K (SOME module_name);
    1.19      val fragments_tab = build_module_namespace { module_prefix = module_prefix,
    1.20        module_identifiers = module_identifiers, reserved = reserved } program;
    1.21 -    val prep_name = force_identifier symbol_of fragments_tab identifiers
    1.22 +    val prep_name = force_identifier symbol_of fragments_tab (Long_Name.explode module_name) identifiers
    1.23        #>> Long_Name.implode;
    1.24  
    1.25      (* distribute statements over hierarchy *)
    1.26 @@ -171,7 +172,7 @@
    1.27        else K (SOME module_name);
    1.28      val fragments_tab = build_module_namespace { module_prefix = "",
    1.29        module_identifiers = module_identifiers, reserved = reserved } program;
    1.30 -    val prep_name = force_identifier symbol_of fragments_tab identifiers;
    1.31 +    val prep_name = force_identifier symbol_of fragments_tab (Long_Name.explode module_name) identifiers;
    1.32  
    1.33      (* building empty module hierarchy *)
    1.34      val empty_module = (empty_data, Graph.empty);