# HG changeset patch
# User blanchet
# Date 1277201946 -7200
# Node ID 650fae5eea93417d3167b4bad429999d9535917a
# Parent  a5aa61b7fa740aca8fea0d49bc421ef116c2e6b7
make the Nitpick_Example theory processable even when Kodkodi is not installed;
so that at least the "theory" aspects of it (as opposed to the diagnosis offered by Nitpick) are checked on everybody's machines

diff -r a5aa61b7fa74 -r 650fae5eea93 src/HOL/Nitpick_Examples/Mini_Nits.thy
--- a/src/HOL/Nitpick_Examples/Mini_Nits.thy	Tue Jun 22 01:21:52 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Mini_Nits.thy	Tue Jun 22 12:19:06 2010 +0200
@@ -14,14 +14,19 @@
 ML {*
 exception FAIL
 
-(* int -> term -> string *)
+val has_kodkodi = (getenv "KODKODI" <> "")
+
 fun minipick n t =
   map (fn k => Minipick.kodkod_problem_from_term @{context} (K k) t) (1 upto n)
   |> Minipick.solve_any_kodkod_problem @{theory}
-(* int -> term -> bool *)
-fun none n t = (minipick n t = "none" orelse raise FAIL)
-fun genuine n t = (minipick n t = "genuine" orelse raise FAIL)
-fun unknown n t = (minipick n t = "unknown" orelse raise FAIL)
+fun minipick_expect expect n t =
+  if has_kodkodi then
+    if minipick n t = expect then () else raise FAIL
+  else
+    ()
+val none = minipick_expect "none"
+val genuine = minipick_expect "genuine"
+val unknown = minipick_expect "unknown"
 *}
 
 ML {* genuine 1 @{prop "x = Not"} *}
diff -r a5aa61b7fa74 -r 650fae5eea93 src/HOL/Nitpick_Examples/ROOT.ML
--- a/src/HOL/Nitpick_Examples/ROOT.ML	Tue Jun 22 01:21:52 2010 +0200
+++ b/src/HOL/Nitpick_Examples/ROOT.ML	Tue Jun 22 12:19:06 2010 +0200
@@ -5,8 +5,4 @@
 Nitpick examples.
 *)
 
-if getenv "KODKODI" = "" then
-  ()
-else
-  setmp_noncritical quick_and_dirty true use_thys
-                    ["Nitpick_Examples"];
+setmp_noncritical quick_and_dirty true use_thys ["Nitpick_Examples"];
diff -r a5aa61b7fa74 -r 650fae5eea93 src/HOL/Nitpick_Examples/Tests_Nits.thy
--- a/src/HOL/Nitpick_Examples/Tests_Nits.thy	Tue Jun 22 01:21:52 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Tests_Nits.thy	Tue Jun 22 12:19:06 2010 +0200
@@ -11,6 +11,6 @@
 imports Main
 begin
 
-ML {* Nitpick_Tests.run_all_tests () *}
+ML {* () |> getenv "KODKODI" <> "" ? Nitpick_Tests.run_all_tests *}
 
 end