equal
deleted
inserted
replaced
513 val cs3 = map_filter (fn (c, name) => |
513 val cs3 = map_filter (fn (c, name) => |
514 if member (op =) names3 name then SOME c else NONE) (cs2 ~~ names2); |
514 if member (op =) names3 name then SOME c else NONE) (cs2 ~~ names2); |
515 in union (op =) cs3 cs1 end; |
515 in union (op =) cs3 cs1 end; |
516 |
516 |
517 fun prep_destination "" = NONE |
517 fun prep_destination "" = NONE |
518 | prep_destination "-" = NONE |
518 | prep_destination "-" = (legacy_feature "drop \"file\" argument entirely instead of \"-\""; NONE) |
519 | prep_destination s = SOME (Path.explode s); |
519 | prep_destination s = SOME (Path.explode s); |
520 |
520 |
521 fun export_code thy cs seris = |
521 fun export_code thy cs seris = |
522 let |
522 let |
523 val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs; |
523 val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs; |
636 fold set_identifier (prep_name_decl thy raw_name_decls) thy; |
636 fold set_identifier (prep_name_decl thy raw_name_decls) thy; |
637 |
637 |
638 val set_identifiers = gen_set_identifiers cert_name_decls; |
638 val set_identifiers = gen_set_identifiers cert_name_decls; |
639 val set_identifiers_cmd = gen_set_identifiers read_name_decls; |
639 val set_identifiers_cmd = gen_set_identifiers read_name_decls; |
640 |
640 |
641 fun add_module_alias_cmd target = fold (fn (sym, name) => |
641 fun add_module_alias_cmd target aliasses = |
642 set_identifier (target, Code_Symbol.Module (sym, if name = "" then NONE else SOME (check_name true name)))); |
642 let |
|
643 val _ = legacy_feature "prefer \"code_identifier\" over \"code_modulename\""; |
|
644 in |
|
645 fold (fn (sym, name) => set_identifier |
|
646 (target, Code_Symbol.Module (sym, if name = "" then NONE else SOME (check_name true name)))) aliasses |
|
647 end; |
643 |
648 |
644 |
649 |
645 (* custom printings *) |
650 (* custom printings *) |
646 |
651 |
647 fun arrange_printings prep_const thy = |
652 fun arrange_printings prep_const thy = |
668 val set_printings = gen_set_printings cert_printings; |
673 val set_printings = gen_set_printings cert_printings; |
669 val set_printings_cmd = gen_set_printings read_printings; |
674 val set_printings_cmd = gen_set_printings read_printings; |
670 |
675 |
671 fun gen_add_syntax Symbol prep_x prep_syn target raw_x some_raw_syn thy = |
676 fun gen_add_syntax Symbol prep_x prep_syn target raw_x some_raw_syn thy = |
672 let |
677 let |
|
678 val _ = legacy_feature "prefer \"code_printing\" for custom serialisations" |
673 val x = prep_x thy raw_x; |
679 val x = prep_x thy raw_x; |
674 in set_printing (target, Symbol (x, Option.map (prep_syn thy x) some_raw_syn)) thy end; |
680 in set_printing (target, Symbol (x, Option.map (prep_syn thy x) some_raw_syn)) thy end; |
675 |
681 |
676 fun gen_add_const_syntax prep_const = |
682 fun gen_add_const_syntax prep_const = |
677 gen_add_syntax Code_Symbol.Constant prep_const check_const_syntax; |
683 gen_add_syntax Code_Symbol.Constant prep_const check_const_syntax; |