444 val setup = |
444 val setup = |
445 Code_Target.add_target |
445 Code_Target.add_target |
446 (target, { serializer = serializer, literals = literals, |
446 (target, { serializer = serializer, literals = literals, |
447 check = { env_var = "ISABELLE_GHC", make_destination = I, |
447 check = { env_var = "ISABELLE_GHC", make_destination = I, |
448 make_command = fn module_name => |
448 make_command = fn module_name => |
449 "\"$ISABELLE_GHC\" -XRankNTypes -XScopedTypeVariables -odir build -hidir build -stubdir build -e \"\" " ^ |
449 "\"$ISABELLE_GHC\" -XRankNTypes -XScopedTypeVariables -XEmptyDataDecls -odir build -hidir build -stubdir build -e \"\" " ^ |
450 module_name ^ ".hs" } }) |
450 module_name ^ ".hs" } }) |
451 #> Code_Target.add_tyco_syntax target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] => |
451 #> Code_Target.add_tyco_syntax target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] => |
452 brackify_infix (1, R) fxy ( |
452 brackify_infix (1, R) fxy ( |
453 print_typ (INFX (1, X)) ty1, |
453 print_typ (INFX (1, X)) ty1, |
454 str "->", |
454 str "->", |