equal
deleted
inserted
replaced
324 val add_include_cmd = gen_add_include Code_Unit.read_const; |
324 val add_include_cmd = gen_add_include Code_Unit.read_const; |
325 |
325 |
326 fun add_module_alias target (thyname, modlname) = |
326 fun add_module_alias target (thyname, modlname) = |
327 let |
327 let |
328 val xs = Long_Name.explode modlname; |
328 val xs = Long_Name.explode modlname; |
329 val xs' = map (Code_Name.purify_name true) xs; |
329 val xs' = map (Name.desymbolize true) xs; |
330 in if xs' = xs |
330 in if xs' = xs |
331 then map_module_alias target (Symtab.update (thyname, modlname)) |
331 then map_module_alias target (Symtab.update (thyname, modlname)) |
332 else error ("Invalid module name: " ^ quote modlname ^ "\n" |
332 else error ("Invalid module name: " ^ quote modlname ^ "\n" |
333 ^ "perhaps try " ^ quote (Long_Name.implode xs')) |
333 ^ "perhaps try " ^ quote (Long_Name.implode xs')) |
334 end; |
334 end; |
500 val names = map_filter (Code_Thingol.lookup_const naming) cs; |
500 val names = map_filter (Code_Thingol.lookup_const naming) cs; |
501 in subtract (op =) (Graph.all_preds program names) (Graph.keys program) end; |
501 in subtract (op =) (Graph.all_preds program names) (Graph.keys program) end; |
502 |
502 |
503 fun read_const_exprs thy cs = |
503 fun read_const_exprs thy cs = |
504 let |
504 let |
505 val (cs1, cs2) = Code_Name.read_const_exprs thy cs; |
505 val (cs1, cs2) = Code_Thingol.read_const_exprs thy cs; |
506 val (names3, (naming, program)) = Code_Thingol.consts_program thy cs2; |
506 val (names3, (naming, program)) = Code_Thingol.consts_program thy cs2; |
507 val names4 = transitivly_non_empty_funs thy naming program; |
507 val names4 = transitivly_non_empty_funs thy naming program; |
508 val cs5 = map_filter |
508 val cs5 = map_filter |
509 (fn (c, name) => if member (op =) names4 name then SOME c else NONE) (cs2 ~~ names3); |
509 (fn (c, name) => if member (op =) names4 name then SOME c else NONE) (cs2 ~~ names3); |
510 in fold (insert (op =)) cs5 cs1 end; |
510 in fold (insert (op =)) cs5 cs1 end; |