# HG changeset patch
# User bulwahn
# Date 1335786510 -7200
# Node ID 4da917ed49b76ca52664a63e07b35eaef11846f0
# Parent  179b5e7c980300f0d5710a14c2e05302678c46cc
adding configuration to pass options to the ghc call in quickcheck[narrowing]

diff -r 179b5e7c9803 -r 4da917ed49b7 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Apr 30 12:14:53 2012 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Apr 30 13:48:30 2012 +0200
@@ -9,6 +9,7 @@
   val allow_existentials : bool Config.T
   val finite_functions : bool Config.T
   val overlord : bool Config.T
+  val ghc_options : string Config.T
   val active : bool Config.T
   datatype counterexample = Universal_Counterexample of (term * counterexample)
     | Existential_Counterexample of (term * counterexample) list
@@ -26,6 +27,7 @@
 val allow_existentials = Attrib.setup_config_bool @{binding quickcheck_allow_existentials} (K true)
 val finite_functions = Attrib.setup_config_bool @{binding quickcheck_finite_functions} (K true)
 val overlord = Attrib.setup_config_bool @{binding quickcheck_narrowing_overlord} (K false)
+val ghc_options = Attrib.setup_config_string @{binding quickcheck_narrowing_ghc_options} (K "")
 
 (* partial_term_of instances *)
 
@@ -231,6 +233,7 @@
     fun excipit () =
       "Quickcheck ran out of time while testing at size " ^ string_of_int (!current_size)
     val tmp_prefix = "Quickcheck_Narrowing"
+    val ghc_options = Config.get ctxt ghc_options
     val with_tmp_dir =
       if Config.get ctxt overlord then with_overlord_dir else Isabelle_System.with_tmp_dir 
     fun run in_path = 
@@ -254,6 +257,7 @@
         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\" " ^ Code_Haskell.language_params ^ " " ^
+          ghc_options ^ " " ^
           (space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^
           " -o " ^ executable ^ ";"
         val (result, compilation_time) =