src/Tools/Code/code_haskell.ML
changeset 44321 975c9ba50a41
parent 43326 47cf4bc789aa
child 44788 8b935f1b3cf8
equal deleted inserted replaced
44320:33439faadd67 44321:975c9ba50a41
   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 "->",