equal
deleted
inserted
replaced
354 activate_syntax (Code_Thingol.lookup_class naming) (Code_Symbol.dest_type_class_data printings); |
354 activate_syntax (Code_Thingol.lookup_class naming) (Code_Symbol.dest_type_class_data printings); |
355 val names_inst = map_filter (Code_Thingol.lookup_instance naming o fst) |
355 val names_inst = map_filter (Code_Thingol.lookup_instance naming o fst) |
356 (Code_Symbol.dest_class_instance_data printings); |
356 (Code_Symbol.dest_class_instance_data printings); |
357 in |
357 in |
358 (names_const @ names_tyco @ names_class @ names_inst, |
358 (names_const @ names_tyco @ names_class @ names_inst, |
359 (const_syntax, tyco_syntax, class_syntax)) |
359 (Symtab.lookup const_syntax, Symtab.lookup tyco_syntax, Symtab.lookup class_syntax)) |
360 end; |
360 end; |
361 |
361 |
362 fun project_program thy names_hidden names1 program2 = |
362 fun project_program thy names_hidden names1 program2 = |
363 let |
363 let |
364 val ctxt = Proof_Context.init_global thy; |
364 val ctxt = Proof_Context.init_global thy; |
390 symbol_of = Code_Thingol.symbol_of proto_program, |
390 symbol_of = Code_Thingol.symbol_of proto_program, |
391 module_name = module_name, |
391 module_name = module_name, |
392 reserved_syms = reserved, |
392 reserved_syms = reserved, |
393 identifiers = identifiers, |
393 identifiers = identifiers, |
394 includes = includes, |
394 includes = includes, |
395 const_syntax = Symtab.lookup const_syntax, |
395 const_syntax = const_syntax, |
396 tyco_syntax = Symtab.lookup tyco_syntax, |
396 tyco_syntax = tyco_syntax, |
397 class_syntax = Symtab.lookup class_syntax }, |
397 class_syntax = class_syntax }, |
398 program) |
398 program) |
399 end; |
399 end; |
400 |
400 |
401 fun mount_serializer thy target some_width module_name args naming program names = |
401 fun mount_serializer thy target some_width module_name args naming program names = |
402 let |
402 let |