1.1 --- a/src/Tools/Code/code_haskell.ML	Wed Sep 14 06:49:24 2011 +0200
     1.2 +++ b/src/Tools/Code/code_haskell.ML	Wed Sep 14 10:24:22 2011 +0200
     1.3 @@ -6,6 +6,7 @@
     1.4  
     1.5  signature CODE_HASKELL =
     1.6  sig
     1.7 +  val language_params: string
     1.8    val target: string
     1.9    val setup: theory -> theory
    1.10  end;
    1.11 @@ -15,6 +16,15 @@
    1.12  
    1.13  val target = "Haskell";
    1.14  
    1.15 +val language_extensions =
    1.16 +    ["EmptyDataDecls", "RankNTypes", "ScopedTypeVariables"];
    1.17 +
    1.18 +val language_pragma =
    1.19 +    "{-# LANGUAGE " ^ commas language_extensions ^ " #-}";
    1.20 +
    1.21 +val language_params =
    1.22 +    space_implode " " (map (prefix "-X") language_extensions);
    1.23 +
    1.24  open Basic_Code_Thingol;
    1.25  open Code_Printer;
    1.26  
    1.27 @@ -348,7 +358,7 @@
    1.28              val _ = Isabelle_System.mkdirs (Path.dir filepath);
    1.29            in
    1.30              (File.write filepath o format [] width o Pretty.chunks2)
    1.31 -              [str "{-# LANGUAGE ScopedTypeVariables #-}", content]
    1.32 +              [str language_pragma, content]
    1.33            end
    1.34        | write_module width NONE (_, content) = writeln (format [] width content);
    1.35    in
    1.36 @@ -446,7 +456,7 @@
    1.37      (target, { serializer = serializer, literals = literals,
    1.38        check = { env_var = "ISABELLE_GHC", make_destination = I,
    1.39          make_command = fn module_name =>
    1.40 -          "\"$ISABELLE_GHC\" -XRankNTypes -XScopedTypeVariables -XEmptyDataDecls -odir build -hidir build -stubdir build -e \"\" " ^
    1.41 +          "\"$ISABELLE_GHC\" " ^ language_params  ^ " -odir build -hidir build -stubdir build -e \"\" " ^
    1.42              module_name ^ ".hs" } })
    1.43    #> Code_Target.add_tyco_syntax target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
    1.44        brackify_infix (1, R) fxy (