# HG changeset patch
# User blanchet
# Date 1256817044 -3600
# Node ID 532b915afa1435028884cec907a4137bff36a8a6
# Parent  3b8fc89a52b78e7254ff6a57eb33f972be615ee5
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)

diff -r 3b8fc89a52b7 -r 532b915afa14 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Thu Oct 29 12:29:31 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Thu Oct 29 12:50:44 2009 +0100
@@ -137,6 +137,15 @@
                                  Pretty.str (if j = 1 then "." else ";")])
                (length ts downto 1) ts))]
 
+(* unit -> string *)
+fun install_kodkodi_message () =
+  "Nitpick requires the external Java program Kodkodi. To install it, download \
+  \the package from Isabelle's web page and add the \"kodkodi-x.y.z\" \
+  \directory's full path to \"" ^
+  Path.implode (Path.expand (Path.appends
+      (Path.variable "ISABELLE_HOME_USER" ::
+       map Path.basic ["etc", "components"]))) ^ "\"."
+
 val max_liberal_delay_ms = 200
 val max_liberal_delay_percent = 2
 
@@ -166,6 +175,9 @@
 val has_weaselly_sorts =
   exists_type o exists_subtype o is_tfree_with_weaselly_sort
 
+(* (unit -> string) -> Pretty.T *)
+fun plazy f = Pretty.blk (0, pstrs (f ()))
+
 (* Time.time -> Proof.state -> params -> bool -> term -> string * Proof.state *)
 fun pick_them_nits_in_term deadline state (params : params) auto orig_assm_ts
                            orig_t =
@@ -198,9 +210,9 @@
     (* string -> unit *)
     val print = pprint o curry Pretty.blk 0 o pstrs
     (* (unit -> string) -> unit *)
-    fun print_m f = pprint_m (curry Pretty.blk 0 o pstrs o f)
-    fun print_v f = pprint_v (curry Pretty.blk 0 o pstrs o f)
-    fun print_d f = pprint_d (curry Pretty.blk 0 o pstrs o f)
+    val print_m = pprint_m o K o plazy
+    val print_v = pprint_v o K o plazy
+    val print_d = pprint_d o K o plazy
 
     (* unit -> unit *)
     fun check_deadline () =
@@ -631,15 +643,7 @@
           case Kodkod.solve_any_problem overlord deadline max_threads
                                         max_solutions (map fst problems) of
             Kodkod.NotInstalled =>
-            (print_m (fn () =>
-                         "Nitpick requires the external Java program Kodkodi. \
-                         \To install it, download the package from Isabelle's \
-                         \web page and add the \"kodkodi-x.y.z\" directory's \
-                         \full path to \"" ^
-                         Path.implode (Path.expand (Path.appends
-                             (Path.variable "ISABELLE_HOME" ::
-                              (map Path.basic ["etc", "components"])))) ^
-                         "\".");
+            (print_m install_kodkodi_message;
              (max_potential, max_genuine, donno + 1))
           | Kodkod.Normal ([], unsat_js) =>
             (update_checked_problems problems unsat_js;
@@ -842,16 +846,21 @@
 (* Proof.state -> params -> bool -> term -> string * Proof.state *)
 fun pick_nits_in_term state (params as {debug, timeout, expect, ...})
                       auto orig_assm_ts orig_t =
-  let
-    val deadline = Option.map (curry Time.+ (Time.now ())) timeout
-    val outcome as (outcome_code, _) =
-      time_limit (if debug then NONE else timeout)
-          (pick_them_nits_in_term deadline state params auto orig_assm_ts)
-          orig_t
-  in
-    if expect = "" orelse outcome_code = expect then outcome
-    else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
-  end
+  if getenv "KODKODI" = "" then
+    (if auto then ()
+     else warning (Pretty.string_of (plazy install_kodkodi_message));
+     ("unknown", state))
+  else
+    let
+      val deadline = Option.map (curry Time.+ (Time.now ())) timeout
+      val outcome as (outcome_code, _) =
+        time_limit (if debug then NONE else timeout)
+            (pick_them_nits_in_term deadline state params auto orig_assm_ts)
+            orig_t
+    in
+      if expect = "" orelse outcome_code = expect then outcome
+      else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
+    end
 
 (* Proof.state -> params -> thm -> int -> string * Proof.state *)
 fun pick_nits_in_subgoal state params auto subgoal =