# HG changeset patch
# User blanchet
# Date 1277205479 -7200
# Node ID 71fdbffe3275bc04d2f3641afcce504061474671
# Parent  9ae78e12e126cb97fc1a5302cc9f4ac4667b81db
distinguish between "unknown" and "no Kodkodi installed" errors

diff -r 9ae78e12e126 -r 71fdbffe3275 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Jun 22 13:17:17 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Jun 22 13:17:59 2010 +0200
@@ -943,15 +943,15 @@
 
 fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto i n
                       step subst orig_assm_ts orig_t =
-  let
-    val warning_m = if auto then K () else warning
-    val unknown_outcome = ("unknown", state)
-  in
+  let val warning_m = if auto then K () else warning in
     if getenv "KODKODI" = "" then
+      (* The "expect" argument is deliberately ignored if Kodkodi is missing so
+         that the "Nitpick_Examples" can be processed on any machine. *)
       (warning_m (Pretty.string_of (plazy install_kodkodi_message));
-       unknown_outcome)
+       ("no_kodkodi", state))
     else
       let
+        val unknown_outcome = ("unknown", state)
         val deadline = Option.map (curry Time.+ (Time.now ())) timeout
         val outcome as (outcome_code, _) =
           time_limit (if debug then NONE else timeout)