src/Tools/Code/code_namespace.ML
changeset 55605 b1b363e81c87
parent 55293 42cf5802d36a
child 55679 59244fc1a7ca
     1.1 --- a/src/Tools/Code/code_namespace.ML	Thu Feb 20 15:14:37 2014 +0100
     1.2 +++ b/src/Tools/Code/code_namespace.ML	Thu Feb 20 10:32:09 2014 +0100
     1.3 @@ -245,17 +245,20 @@
     1.4          val (nsps', nodes') = (nsps, nodes)
     1.5            |> fold (declare (K namify_module)) module_fragments
     1.6            |> fold (declare (namify_stmt o (fn Stmt stmt => stmt))) stmt_syms;
     1.7 -        fun zip_fillup xs ys = xs ~~ ys @ replicate (length xs - length ys) NONE;
     1.8          fun select_syms syms = case filter (member (op =) stmt_syms) syms
     1.9           of [] => NONE
    1.10            | syms => SOME syms;
    1.11 -        val modify_stmts' = AList.make (snd o Code_Symbol.Graph.get_node nodes)
    1.12 -          #> split_list
    1.13 -          ##> map (fn Stmt stmt => stmt)
    1.14 -          #> (fn (syms, stmts) => zip_fillup syms (modify_stmts (syms ~~ stmts)));
    1.15 +        fun select_stmt (sym, SOME stmt) = SOME (sym, stmt)
    1.16 +          | select_stmt _ = NONE;
    1.17 +        fun modify_stmts' syms =
    1.18 +          let
    1.19 +            val stmts = map ((fn Stmt stmt => stmt) o snd o Code_Symbol.Graph.get_node nodes) syms;
    1.20 +            val stmts' = modify_stmts (syms ~~ stmts);
    1.21 +            val stmts'' = stmts' @ replicate (length syms - length stmts') NONE;
    1.22 +          in map_filter select_stmt (syms ~~ stmts'') end;
    1.23          val stmtss' = (maps modify_stmts' o map_filter select_syms o Code_Symbol.Graph.strong_conn) nodes;
    1.24          val nodes'' = Code_Symbol.Graph.map (fn sym => apsnd (fn Module content => Module (make_declarations nsps' content)
    1.25 -            | _ => case AList.lookup (op =) stmtss' sym of SOME (SOME stmt) => Stmt stmt | _ => Dummy)) nodes';
    1.26 +            | _ => case AList.lookup (op =) stmtss' sym of SOME stmt => Stmt stmt | _ => Dummy)) nodes';
    1.27          val data' = fold memorize_data stmt_syms data;
    1.28        in (data', nodes'') end;
    1.29      val (_, hierarchical_program) = make_declarations empty_nsp proto_program;