src/Tools/Code/code_namespace.ML
changeset 55150 0940309ed8f1
parent 55147 bce3dbc11f95
child 55291 82780e5f7622
     1.1 --- a/src/Tools/Code/code_namespace.ML	Sat Jan 25 23:50:49 2014 +0100
     1.2 +++ b/src/Tools/Code/code_namespace.ML	Sat Jan 25 23:50:49 2014 +0100
     1.3 @@ -13,7 +13,7 @@
     1.4      namify_stmt: Code_Thingol.stmt -> string -> 'a -> string * 'a,
     1.5      modify_stmt: Code_Thingol.stmt -> Code_Thingol.stmt option }
     1.6        -> Code_Thingol.program
     1.7 -      -> { deresolver: string -> Code_Symbol.symbol -> string,
     1.8 +      -> { deresolver: string -> Code_Symbol.T -> string,
     1.9             flat_program: flat_program }
    1.10  
    1.11    datatype ('a, 'b) node =
    1.12 @@ -26,13 +26,13 @@
    1.13      reserved: Name.context, identifiers: Code_Target.identifier_data,
    1.14      empty_nsp: 'c, namify_module: string -> 'c -> string * 'c,
    1.15      namify_stmt: Code_Thingol.stmt -> string -> 'c -> string * 'c,
    1.16 -    cyclic_modules: bool, empty_data: 'b, memorize_data: Code_Symbol.symbol -> 'b -> 'b,
    1.17 -    modify_stmts: (Code_Symbol.symbol * Code_Thingol.stmt) list -> 'a option list }
    1.18 +    cyclic_modules: bool, empty_data: 'b, memorize_data: Code_Symbol.T -> 'b -> 'b,
    1.19 +    modify_stmts: (Code_Symbol.T * Code_Thingol.stmt) list -> 'a option list }
    1.20        -> Code_Thingol.program
    1.21 -      -> { deresolver: string list -> Code_Symbol.symbol -> string,
    1.22 +      -> { deresolver: string list -> Code_Symbol.T -> string,
    1.23             hierarchical_program: ('a, 'b) hierarchical_program }
    1.24    val print_hierarchical: { print_module: string list -> string -> 'b -> 'c list -> 'c,
    1.25 -    print_stmt: string list -> Code_Symbol.symbol * 'a -> 'c,
    1.26 +    print_stmt: string list -> Code_Symbol.T * 'a -> 'c,
    1.27      lift_markup: (Pretty.T -> Pretty.T) -> 'c -> 'c }
    1.28        -> ('a, 'b) hierarchical_program -> 'c list
    1.29  end;
    1.30 @@ -48,7 +48,7 @@
    1.31  
    1.32  fun force_identifier ctxt fragments_tab force_module identifiers sym =
    1.33    case lookup_identifier identifiers sym of
    1.34 -      NONE => ((the o Symtab.lookup fragments_tab o Code_Symbol.namespace_prefix ctxt) sym, Code_Symbol.base_name sym)
    1.35 +      NONE => ((the o Symtab.lookup fragments_tab o Code_Symbol.default_prefix ctxt) sym, Code_Symbol.default_base sym)
    1.36      | SOME prefix_name => if null force_module then prefix_name
    1.37          else (force_module, snd prefix_name);
    1.38  
    1.39 @@ -57,7 +57,7 @@
    1.40      fun alias_fragments name = case module_identifiers name
    1.41       of SOME name' => Long_Name.explode name'
    1.42        | NONE => map (fn name => fst (Name.variant name reserved)) (Long_Name.explode name);
    1.43 -    val module_names = Code_Symbol.Graph.fold (insert (op =) o Code_Symbol.namespace_prefix ctxt o fst) program [];
    1.44 +    val module_names = Code_Symbol.Graph.fold (insert (op =) o Code_Symbol.default_prefix ctxt o fst) program [];
    1.45    in
    1.46      fold (fn name => Symtab.update (name, Long_Name.explode module_prefix @ alias_fragments name))
    1.47        module_names Symtab.empty
    1.48 @@ -66,7 +66,7 @@
    1.49  
    1.50  (** flat program structure **)
    1.51  
    1.52 -type flat_program = ((string * Code_Thingol.stmt option) Code_Symbol.Graph.T * (string * Code_Symbol.symbol list) list) Graph.T;
    1.53 +type flat_program = ((string * Code_Thingol.stmt option) Code_Symbol.Graph.T * (string * Code_Symbol.T list) list) Graph.T;
    1.54  
    1.55  fun flat_program ctxt { module_prefix, module_name, reserved,
    1.56      identifiers, empty_nsp, namify_stmt, modify_stmt } program =