src/Tools/Code/code_haskell.ML
changeset 38863 9070a7c356c9
parent 38779 89f654951200
child 38910 6af1d8673cbf
equal deleted inserted replaced
38862:2795499a20bd 38863:9070a7c356c9
   481 
   481 
   482 val setup =
   482 val setup =
   483   Code_Target.add_target
   483   Code_Target.add_target
   484     (target, { serializer = isar_serializer, literals = literals,
   484     (target, { serializer = isar_serializer, literals = literals,
   485       check = { env_var = "EXEC_GHC", make_destination = I,
   485       check = { env_var = "EXEC_GHC", make_destination = I,
   486         make_command = fn ghc => fn p => fn module_name =>
   486         make_command = fn ghc => fn module_name =>
   487           ghc ^ " -fglasgow-exts -odir build -hidir build -stubdir build -e \"\" " ^ module_name ^ ".hs" } })
   487           ghc ^ " -fglasgow-exts -odir build -hidir build -stubdir build -e \"\" " ^ module_name ^ ".hs" } })
   488   #> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
   488   #> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
   489       brackify_infix (1, R) fxy (
   489       brackify_infix (1, R) fxy (
   490         print_typ (INFX (1, X)) ty1,
   490         print_typ (INFX (1, X)) ty1,
   491         str "->",
   491         str "->",