451 val setup = |
451 val setup = |
452 Code_Target.add_target |
452 Code_Target.add_target |
453 (target, { serializer = serializer, literals = literals, |
453 (target, { serializer = serializer, literals = literals, |
454 check = { env_var = "ISABELLE_GHC", make_destination = I, |
454 check = { env_var = "ISABELLE_GHC", make_destination = I, |
455 make_command = fn module_name => |
455 make_command = fn module_name => |
456 "\"$ISABELLE_GHC\" -fglasgow-exts -odir build -hidir build -stubdir build -e \"\" " ^ |
456 "\"$ISABELLE_GHC\" -XRankNTypes -XScopedTypeVariables -odir build -hidir build -stubdir build -e \"\" " ^ |
457 module_name ^ ".hs" } }) |
457 module_name ^ ".hs" } }) |
458 #> Code_Target.add_tyco_syntax target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] => |
458 #> Code_Target.add_tyco_syntax target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] => |
459 brackify_infix (1, R) fxy ( |
459 brackify_infix (1, R) fxy ( |
460 print_typ (INFX (1, X)) ty1, |
460 print_typ (INFX (1, X)) ty1, |
461 str "->", |
461 str "->", |