src/Tools/Code/code_target.ML
changeset 37972 f37a8d488105
parent 37898 eb89d0ac75fb
child 38779 89f654951200
equal deleted inserted replaced
37971:278367fa09f3 37972:f37a8d488105
   139     Target { serial = serial2, description = _,
   139     Target { serial = serial2, description = _,
   140       reserved = reserved2, includes = includes2,
   140       reserved = reserved2, includes = includes2,
   141       name_syntax_table = name_syntax_table2, module_alias = module_alias2 }) =
   141       name_syntax_table = name_syntax_table2, module_alias = module_alias2 }) =
   142   if serial1 = serial2 orelse not strict then
   142   if serial1 = serial2 orelse not strict then
   143     make_target ((serial1, description),
   143     make_target ((serial1, description),
   144       ((merge (op =) (reserved1, reserved2), Symtab.merge (K true) (includes1, includes2)),
   144       ((merge (op =) (reserved1, reserved2), Symtab.join (K snd) (includes1, includes2)),
   145         (merge_name_syntax_table (name_syntax_table1, name_syntax_table2),
   145         (merge_name_syntax_table (name_syntax_table1, name_syntax_table2),
   146           Symtab.join (K fst) (module_alias1, module_alias2))
   146           Symtab.join (K snd) (module_alias1, module_alias2))
   147     ))
   147     ))
   148   else
   148   else
   149     error ("Incompatible targets: " ^ quote target);
   149     error ("Incompatible targets: " ^ quote target);
   150 
   150 
   151 fun the_description (Target { description, ... }) = description;
   151 fun the_description (Target { description, ... }) = description;