# HG changeset patch
# User haftmann
# Date 1283346583 -7200
# Node ID 5681d7cfabceb3a2474b4348c3d31babdc0e1e64
# Parent  8cd5b6d688fa25211363d1d6ea75ace9cf136780
tuned

diff -r 8cd5b6d688fa -r 5681d7cfabce src/Tools/Code/code_namespace.ML
--- a/src/Tools/Code/code_namespace.ML	Wed Sep 01 12:27:49 2010 +0200
+++ b/src/Tools/Code/code_namespace.ML	Wed Sep 01 15:09:43 2010 +0200
@@ -29,6 +29,13 @@
   | Stmt of 'a
   | Module of ('b * (string * ('a, 'b) node) Graph.T);
 
+fun map_module_content f (Module content) = Module (f content);
+
+fun map_module [] = I
+  | map_module (name_fragment :: name_fragments) =
+      apsnd o Graph.map_node name_fragment o apsnd o map_module_content
+        o map_module name_fragments;
+
 fun hierarchical_program labelled_name { module_alias, reserved, empty_nsp,
       namify_module, namify_stmt, cyclic_modules, empty_data, memorize_data } program =
   let
@@ -45,11 +52,6 @@
 
     (* building empty module hierarchy *)
     val empty_module = (empty_data, Graph.empty);
-    fun map_module f (Module content) = Module (f content);
-    fun change_module [] = I
-      | change_module (name_fragment :: name_fragments) =
-          apsnd o Graph.map_node name_fragment o apsnd o map_module
-            o change_module name_fragments;
     fun ensure_module name_fragment (data, nodes) =
       if can (Graph.get_node nodes) name_fragment then (data, nodes)
       else (data,
@@ -57,7 +59,7 @@
     fun allocate_module [] = I
       | allocate_module (name_fragment :: name_fragments) =
           ensure_module name_fragment
-          #> (apsnd o Graph.map_node name_fragment o apsnd o map_module o allocate_module) name_fragments;
+          #> (apsnd o Graph.map_node name_fragment o apsnd o map_module_content o allocate_module) name_fragments;
     val empty_program = Symtab.fold (fn (_, fragments) => allocate_module fragments)
       fragments_tab empty_module;
 
@@ -66,8 +68,7 @@
       let
         val (name_fragments, base) = dest_name name;
       in
-        change_module name_fragments (fn (data, nodes) =>
-          (memorize_data name data, Graph.new_node (name, (base, Stmt stmt)) nodes))
+        (map_module name_fragments o apsnd) (Graph.new_node (name, (base, Stmt stmt)))
       end;
     fun add_dependency name name' =
       let
@@ -83,7 +84,7 @@
               ^ quote name ^ " -> " ^ quote name'
               ^ " would result in module dependency cycle"))
           else Graph.add_edge dep
-      in (change_module name_fragments_common o apsnd) add_edge end;
+      in (map_module name_fragments_common o apsnd) add_edge end;
     val proto_program = empty_program
       |> Graph.fold (fn (name, (stmt, _)) => add_stmt name stmt) program
       |> Graph.fold (fn (name, (_, (_, names))) => fold (add_dependency name) names) program;
@@ -109,8 +110,9 @@
           |> fold (declare (namify_stmt o (fn Stmt stmt => stmt)) modify_stmt) stmt_names;
         val nodes'' = nodes'
           |> fold (fn name_fragment => (Graph.map_node name_fragment
-              o apsnd o map_module) (make_declarations nsps')) module_fragments;
-      in (data, nodes'') end;
+              o apsnd o map_module_content) (make_declarations nsps')) module_fragments;
+        val data' = fold memorize_data stmt_names data;
+      in (data', nodes'') end;
     val (_, hierarchical_program) = make_declarations empty_nsp proto_program;
 
     (* deresolving *)