fixed spying so that the envirnoment variables are queried at run-time not at build-time
authorblanchet
Thu Nov 21 12:29:29 2013 +0100 (2013-11-21 ago)
changeset 545468b403a7a8c44
parent 54545 483131676087
child 54547 c999e2533487
fixed spying so that the envirnoment variables are queried at run-time not at build-time
src/HOL/Tools/Nitpick/nitpick_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Wed Nov 20 23:14:06 2013 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Thu Nov 21 12:29:29 2013 +0100
     1.3 @@ -144,10 +144,7 @@
     1.4  structure Data = Theory_Data
     1.5  (
     1.6    type T = raw_param list
     1.7 -  val empty =
     1.8 -    default_default_params
     1.9 -    |> getenv "NITPICK_SPY" = "yes" ? AList.update (op =) ("spy", "true")
    1.10 -    |> map (apsnd single)
    1.11 +  val empty = default_default_params |> map (apsnd single)
    1.12    val extend = I
    1.13    fun merge data = AList.merge (op =) (K true) data
    1.14  )
    1.15 @@ -258,7 +255,7 @@
    1.16      val debug = (mode <> Auto_Try andalso lookup_bool "debug")
    1.17      val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose")
    1.18      val overlord = lookup_bool "overlord"
    1.19 -    val spy = lookup_bool "spy"
    1.20 +    val spy = getenv "NITPICK_SPY" = "yes" orelse lookup_bool "spy"
    1.21      val user_axioms = lookup_bool_option "user_axioms"
    1.22      val assms = lookup_bool "assms"
    1.23      val whacks = lookup_term_list_option_polymorphic "whack" |> these
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Nov 20 23:14:06 2013 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Nov 21 12:29:29 2013 +0100
     2.3 @@ -187,10 +187,7 @@
     2.4  structure Data = Theory_Data
     2.5  (
     2.6    type T = raw_param list
     2.7 -  val empty =
     2.8 -    default_default_params
     2.9 -    |> getenv "SLEDGEHAMMER_SPY" = "yes" ? AList.update (op =) ("spy", "true")
    2.10 -    |> map (apsnd single)
    2.11 +  val empty = default_default_params |> map (apsnd single)
    2.12    val extend = I
    2.13    fun merge data : T = AList.merge (op =) (K true) data
    2.14  )
    2.15 @@ -265,7 +262,7 @@
    2.16      val debug = mode <> Auto_Try andalso lookup_bool "debug"
    2.17      val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose")
    2.18      val overlord = lookup_bool "overlord"
    2.19 -    val spy = lookup_bool "spy"
    2.20 +    val spy = getenv "SLEDGEHAMMER_SPY" = "yes" orelse lookup_bool "spy"
    2.21      val blocking =
    2.22        Isabelle_Process.is_active () orelse mode <> Normal orelse debug orelse
    2.23        lookup_bool "blocking"