equal
deleted
inserted
replaced
472 |
472 |
473 |
473 |
474 |
474 |
475 (** Isar setup **) |
475 (** Isar setup **) |
476 |
476 |
477 fun isar_seri_haskell module_name = |
477 fun isar_serializer module_name = |
478 Code_Target.parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name) |
478 Code_Target.parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name) |
479 -- Scan.optional (Args.$$$ "string_classes" >> K true) false |
479 -- Scan.optional (Args.$$$ "string_classes" >> K true) false |
480 >> (fn (module_prefix, string_classes) => |
480 >> (fn (module_prefix, string_classes) => |
481 serialize_haskell module_prefix module_name string_classes)); |
481 serialize_haskell module_prefix module_name string_classes)); |
482 |
482 |
485 Parse.term_group -- Parse.name >> (fn (raw_bind, target) => |
485 Parse.term_group -- Parse.name >> (fn (raw_bind, target) => |
486 Toplevel.theory (add_monad target raw_bind)) |
486 Toplevel.theory (add_monad target raw_bind)) |
487 ); |
487 ); |
488 |
488 |
489 val setup = |
489 val setup = |
490 Code_Target.add_target (target, (isar_seri_haskell, literals)) |
490 Code_Target.add_target |
|
491 (target, { serializer = isar_serializer, literals = literals, check = () }) |
491 #> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] => |
492 #> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] => |
492 brackify_infix (1, R) fxy ( |
493 brackify_infix (1, R) fxy ( |
493 print_typ (INFX (1, X)) ty1, |
494 print_typ (INFX (1, X)) ty1, |
494 str "->", |
495 str "->", |
495 print_typ (INFX (1, R)) ty2 |
496 print_typ (INFX (1, R)) ty2 |