Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fixed spying so that the envirnoment variables are queried at run-time not at build-time
authorblanchet
Thu, 21 Nov 2013 12:29:29 +0100
changeset 54546 8b403a7a8c44
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 file | annotate | diff | comparison | revisions
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Wed Nov 20 23:14:06 2013 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Thu Nov 21 12:29:29 2013 +0100
@@ -144,10 +144,7 @@
 structure Data = Theory_Data
 (
   type T = raw_param list
-  val empty =
-    default_default_params
-    |> getenv "NITPICK_SPY" = "yes" ? AList.update (op =) ("spy", "true")
-    |> map (apsnd single)
+  val empty = default_default_params |> map (apsnd single)
   val extend = I
   fun merge data = AList.merge (op =) (K true) data
 )
@@ -258,7 +255,7 @@
     val debug = (mode <> Auto_Try andalso lookup_bool "debug")
     val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose")
     val overlord = lookup_bool "overlord"
-    val spy = lookup_bool "spy"
+    val spy = getenv "NITPICK_SPY" = "yes" orelse lookup_bool "spy"
     val user_axioms = lookup_bool_option "user_axioms"
     val assms = lookup_bool "assms"
     val whacks = lookup_term_list_option_polymorphic "whack" |> these
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Nov 20 23:14:06 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Nov 21 12:29:29 2013 +0100
@@ -187,10 +187,7 @@
 structure Data = Theory_Data
 (
   type T = raw_param list
-  val empty =
-    default_default_params
-    |> getenv "SLEDGEHAMMER_SPY" = "yes" ? AList.update (op =) ("spy", "true")
-    |> map (apsnd single)
+  val empty = default_default_params |> map (apsnd single)
   val extend = I
   fun merge data : T = AList.merge (op =) (K true) data
 )
@@ -265,7 +262,7 @@
     val debug = mode <> Auto_Try andalso lookup_bool "debug"
     val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose")
     val overlord = lookup_bool "overlord"
-    val spy = lookup_bool "spy"
+    val spy = getenv "SLEDGEHAMMER_SPY" = "yes" orelse lookup_bool "spy"
     val blocking =
       Isabelle_Process.is_active () orelse mode <> Normal orelse debug orelse
       lookup_bool "blocking"
isabelle