1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Sep 14 06:49:24 2011 +0200
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Sep 14 10:24:22 2011 +0200
     1.3 @@ -251,7 +251,7 @@
     1.4            (if contains_existentials then pnf_narrowing_engine else narrowing_engine)
     1.5          val _ = File.write main_file main
     1.6          val executable = File.shell_path (Path.append in_path (Path.basic "isabelle_quickcheck_narrowing"))
     1.7 -        val cmd = "exec \"$ISABELLE_GHC\" -XRankNTypes -XScopedTypeVariables -XEmptyDataDecls " ^
     1.8 +        val cmd = "exec \"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^
     1.9            (space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^
    1.10            " -o " ^ executable ^ ";"
    1.11          val (result, compilation_time) =

     2.1 --- a/src/Tools/Code/code_haskell.ML	Wed Sep 14 06:49:24 2011 +0200
     2.2 +++ b/src/Tools/Code/code_haskell.ML	Wed Sep 14 10:24:22 2011 +0200
     2.3 @@ -6,6 +6,7 @@
     2.4  
     2.5  signature CODE_HASKELL =
     2.6  sig
     2.7 +  val language_params: string
     2.8    val target: string
     2.9    val setup: theory -> theory
    2.10  end;
    2.11 @@ -15,6 +16,15 @@
    2.12  
    2.13  val target = "Haskell";
    2.14  
    2.15 +val language_extensions =
    2.16 +    ["EmptyDataDecls", "RankNTypes", "ScopedTypeVariables"];
    2.17 +
    2.18 +val language_pragma =
    2.19 +    "{-# LANGUAGE " ^ commas language_extensions ^ " #-}";
    2.20 +
    2.21 +val language_params =
    2.22 +    space_implode " " (map (prefix "-X") language_extensions);
    2.23 +
    2.24  open Basic_Code_Thingol;
    2.25  open Code_Printer;
    2.26  
    2.27 @@ -348,7 +358,7 @@
    2.28              val _ = Isabelle_System.mkdirs (Path.dir filepath);
    2.29            in
    2.30              (File.write filepath o format [] width o Pretty.chunks2)
    2.31 -              [str "{-# LANGUAGE ScopedTypeVariables #-}", content]
    2.32 +              [str language_pragma, content]
    2.33            end
    2.34        | write_module width NONE (_, content) = writeln (format [] width content);
    2.35    in
    2.36 @@ -446,7 +456,7 @@
    2.37      (target, { serializer = serializer, literals = literals,
    2.38        check = { env_var = "ISABELLE_GHC", make_destination = I,
    2.39          make_command = fn module_name =>
    2.40 -          "\"$ISABELLE_GHC\" -XRankNTypes -XScopedTypeVariables -XEmptyDataDecls -odir build -hidir build -stubdir build -e \"\" " ^
    2.41 +          "\"$ISABELLE_GHC\" " ^ language_params  ^ " -odir build -hidir build -stubdir build -e \"\" " ^
    2.42              module_name ^ ".hs" } })
    2.43    #> Code_Target.add_tyco_syntax target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
    2.44        brackify_infix (1, R) fxy (