# HG changeset patch
# User noschinl
# Date 1315990507 -7200
# Node ID 8bf41f8cf71d10038bb24fa8bcb25998cc242dcb
# Parent  de3ed037c9a5be80c98e3604205db231b44789d6# Parent  1db6baa40b0e72ffde4c1603111a1abb454bcec1
merged

diff -r 1db6baa40b0e -r 8bf41f8cf71d src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Sep 14 09:46:59 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Sep 14 10:55:07 2011 +0200
@@ -251,7 +251,7 @@
           (if contains_existentials then pnf_narrowing_engine else narrowing_engine)
         val _ = File.write main_file main
         val executable = File.shell_path (Path.append in_path (Path.basic "isabelle_quickcheck_narrowing"))
-        val cmd = "exec \"$ISABELLE_GHC\" -XRankNTypes -XScopedTypeVariables -XEmptyDataDecls " ^
+        val cmd = "exec \"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^
           (space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^
           " -o " ^ executable ^ ";"
         val (result, compilation_time) =
diff -r 1db6baa40b0e -r 8bf41f8cf71d src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Wed Sep 14 09:46:59 2011 +0200
+++ b/src/Tools/Code/code_haskell.ML	Wed Sep 14 10:55:07 2011 +0200
@@ -6,6 +6,7 @@
 
 signature CODE_HASKELL =
 sig
+  val language_params: string
   val target: string
   val setup: theory -> theory
 end;
@@ -15,6 +16,15 @@
 
 val target = "Haskell";
 
+val language_extensions =
+    ["EmptyDataDecls", "RankNTypes", "ScopedTypeVariables"];
+
+val language_pragma =
+    "{-# LANGUAGE " ^ commas language_extensions ^ " #-}";
+
+val language_params =
+    space_implode " " (map (prefix "-X") language_extensions);
+
 open Basic_Code_Thingol;
 open Code_Printer;
 
@@ -348,7 +358,7 @@
             val _ = Isabelle_System.mkdirs (Path.dir filepath);
           in
             (File.write filepath o format [] width o Pretty.chunks2)
-              [str "{-# LANGUAGE ScopedTypeVariables #-}", content]
+              [str language_pragma, content]
           end
       | write_module width NONE (_, content) = writeln (format [] width content);
   in
@@ -446,7 +456,7 @@
     (target, { serializer = serializer, literals = literals,
       check = { env_var = "ISABELLE_GHC", make_destination = I,
         make_command = fn module_name =>
-          "\"$ISABELLE_GHC\" -XRankNTypes -XScopedTypeVariables -XEmptyDataDecls -odir build -hidir build -stubdir build -e \"\" " ^
+          "\"$ISABELLE_GHC\" " ^ language_params  ^ " -odir build -hidir build -stubdir build -e \"\" " ^
             module_name ^ ".hs" } })
   #> Code_Target.add_tyco_syntax target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
       brackify_infix (1, R) fxy (