src/Tools/Code/code_namespace.ML
changeset 39055 81e0368812ad
parent 39029 cef7b58555aa
child 39147 3c284a152bd6
     1.1 --- a/src/Tools/Code/code_namespace.ML	Thu Sep 02 12:30:22 2010 +0200
     1.2 +++ b/src/Tools/Code/code_namespace.ML	Thu Sep 02 13:43:38 2010 +0200
     1.3 @@ -6,6 +6,7 @@
     1.4  
     1.5  signature CODE_NAMESPACE =
     1.6  sig
     1.7 +  val dest_name: string -> string * string
     1.8    datatype ('a, 'b) node =
     1.9        Dummy
    1.10      | Stmt of 'a
    1.11 @@ -23,7 +24,13 @@
    1.12  structure Code_Namespace : CODE_NAMESPACE =
    1.13  struct
    1.14  
    1.15 -(* hierarchical program structure *)
    1.16 +(** splitting names in module and base part **)
    1.17 +
    1.18 +val dest_name =
    1.19 +  apfst Long_Name.implode o split_last o fst o split_last o Long_Name.explode;
    1.20 +
    1.21 +
    1.22 +(** hierarchical program structure **)
    1.23  
    1.24  datatype ('a, 'b) node =
    1.25      Dummy
    1.26 @@ -46,10 +53,10 @@
    1.27       of SOME name' => Long_Name.explode name'
    1.28        | NONE => map (fn name => fst (yield_singleton Name.variants name reserved))
    1.29            (Long_Name.explode name);
    1.30 -    val module_names = Graph.fold (insert (op =) o fst o Code_Printer.dest_name o fst) program [];
    1.31 +    val module_names = Graph.fold (insert (op =) o fst o dest_name o fst) program [];
    1.32      val fragments_tab = fold (fn name => Symtab.update
    1.33        (name, alias_fragments name)) module_names Symtab.empty;
    1.34 -    val dest_name = Code_Printer.dest_name #>> (the o Symtab.lookup fragments_tab);
    1.35 +    val dest_name = dest_name #>> (the o Symtab.lookup fragments_tab);
    1.36  
    1.37      (* building empty module hierarchy *)
    1.38      val empty_module = (empty_data, Graph.empty);