src/Tools/Code/code_namespace.ML
changeset 40705 03f1266a066e
parent 40630 3b5c31e55540
child 43326 47cf4bc789aa
equal deleted inserted replaced
40691:a68f64f99832 40705:03f1266a066e
   119               (base_deresolver name))) imported_names
   119               (base_deresolver name))) imported_names
   120       end;
   120       end;
   121     val deresolver_tab = Symtab.make (AList.make
   121     val deresolver_tab = Symtab.make (AList.make
   122       (uncurry classify_names o Graph.get_node flat_program)
   122       (uncurry classify_names o Graph.get_node flat_program)
   123         (Graph.keys flat_program));
   123         (Graph.keys flat_program));
   124     fun deresolver module_name name =
   124     fun deresolver "" name =
   125       the (Symtab.lookup (the (Symtab.lookup deresolver_tab module_name)) name)
   125           Long_Name.append (fst (dest_name name)) (base_deresolver name)
   126       handle Option => error ("Unknown statement name: " ^ labelled_name name);
   126       | deresolver module_name name =
       
   127           the (Symtab.lookup (the (Symtab.lookup deresolver_tab module_name)) name)
       
   128           handle Option => error ("Unknown statement name: " ^ labelled_name name);
   127 
   129 
   128   in { deresolver = deresolver, flat_program = flat_program } end;
   130   in { deresolver = deresolver, flat_program = flat_program } end;
   129 
   131 
   130 
   132 
   131 (** hierarchical program structure **)
   133 (** hierarchical program structure **)