1.1 --- a/src/Tools/Code/code_namespace.ML	Wed Sep 01 12:27:49 2010 +0200
     1.2 +++ b/src/Tools/Code/code_namespace.ML	Wed Sep 01 15:09:43 2010 +0200
     1.3 @@ -29,6 +29,13 @@
     1.4    | Stmt of 'a
     1.5    | Module of ('b * (string * ('a, 'b) node) Graph.T);
     1.6  
     1.7 +fun map_module_content f (Module content) = Module (f content);
     1.8 +
     1.9 +fun map_module [] = I
    1.10 +  | map_module (name_fragment :: name_fragments) =
    1.11 +      apsnd o Graph.map_node name_fragment o apsnd o map_module_content
    1.12 +        o map_module name_fragments;
    1.13 +
    1.14  fun hierarchical_program labelled_name { module_alias, reserved, empty_nsp,
    1.15        namify_module, namify_stmt, cyclic_modules, empty_data, memorize_data } program =
    1.16    let
    1.17 @@ -45,11 +52,6 @@
    1.18  
    1.19      (* building empty module hierarchy *)
    1.20      val empty_module = (empty_data, Graph.empty);
    1.21 -    fun map_module f (Module content) = Module (f content);
    1.22 -    fun change_module [] = I
    1.23 -      | change_module (name_fragment :: name_fragments) =
    1.24 -          apsnd o Graph.map_node name_fragment o apsnd o map_module
    1.25 -            o change_module name_fragments;
    1.26      fun ensure_module name_fragment (data, nodes) =
    1.27        if can (Graph.get_node nodes) name_fragment then (data, nodes)
    1.28        else (data,
    1.29 @@ -57,7 +59,7 @@
    1.30      fun allocate_module [] = I
    1.31        | allocate_module (name_fragment :: name_fragments) =
    1.32            ensure_module name_fragment
    1.33 -          #> (apsnd o Graph.map_node name_fragment o apsnd o map_module o allocate_module) name_fragments;
    1.34 +          #> (apsnd o Graph.map_node name_fragment o apsnd o map_module_content o allocate_module) name_fragments;
    1.35      val empty_program = Symtab.fold (fn (_, fragments) => allocate_module fragments)
    1.36        fragments_tab empty_module;
    1.37  
    1.38 @@ -66,8 +68,7 @@
    1.39        let
    1.40          val (name_fragments, base) = dest_name name;
    1.41        in
    1.42 -        change_module name_fragments (fn (data, nodes) =>
    1.43 -          (memorize_data name data, Graph.new_node (name, (base, Stmt stmt)) nodes))
    1.44 +        (map_module name_fragments o apsnd) (Graph.new_node (name, (base, Stmt stmt)))
    1.45        end;
    1.46      fun add_dependency name name' =
    1.47        let
    1.48 @@ -83,7 +84,7 @@
    1.49                ^ quote name ^ " -> " ^ quote name'
    1.50                ^ " would result in module dependency cycle"))
    1.51            else Graph.add_edge dep
    1.52 -      in (change_module name_fragments_common o apsnd) add_edge end;
    1.53 +      in (map_module name_fragments_common o apsnd) add_edge end;
    1.54      val proto_program = empty_program
    1.55        |> Graph.fold (fn (name, (stmt, _)) => add_stmt name stmt) program
    1.56        |> Graph.fold (fn (name, (_, (_, names))) => fold (add_dependency name) names) program;
    1.57 @@ -109,8 +110,9 @@
    1.58            |> fold (declare (namify_stmt o (fn Stmt stmt => stmt)) modify_stmt) stmt_names;
    1.59          val nodes'' = nodes'
    1.60            |> fold (fn name_fragment => (Graph.map_node name_fragment
    1.61 -              o apsnd o map_module) (make_declarations nsps')) module_fragments;
    1.62 -      in (data, nodes'') end;
    1.63 +              o apsnd o map_module_content) (make_declarations nsps')) module_fragments;
    1.64 +        val data' = fold memorize_data stmt_names data;
    1.65 +      in (data', nodes'') end;
    1.66      val (_, hierarchical_program) = make_declarations empty_nsp proto_program;
    1.67  
    1.68      (* deresolving *)