1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Thu Oct 29 12:29:31 2009 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Thu Oct 29 12:50:44 2009 +0100
     1.3 @@ -137,6 +137,15 @@
     1.4                                   Pretty.str (if j = 1 then "." else ";")])
     1.5                 (length ts downto 1) ts))]
     1.6  
     1.7 +(* unit -> string *)
     1.8 +fun install_kodkodi_message () =
     1.9 +  "Nitpick requires the external Java program Kodkodi. To install it, download \
    1.10 +  \the package from Isabelle's web page and add the \"kodkodi-x.y.z\" \
    1.11 +  \directory's full path to \"" ^
    1.12 +  Path.implode (Path.expand (Path.appends
    1.13 +      (Path.variable "ISABELLE_HOME_USER" ::
    1.14 +       map Path.basic ["etc", "components"]))) ^ "\"."
    1.15 +
    1.16  val max_liberal_delay_ms = 200
    1.17  val max_liberal_delay_percent = 2
    1.18  
    1.19 @@ -166,6 +175,9 @@
    1.20  val has_weaselly_sorts =
    1.21    exists_type o exists_subtype o is_tfree_with_weaselly_sort
    1.22  
    1.23 +(* (unit -> string) -> Pretty.T *)
    1.24 +fun plazy f = Pretty.blk (0, pstrs (f ()))
    1.25 +
    1.26  (* Time.time -> Proof.state -> params -> bool -> term -> string * Proof.state *)
    1.27  fun pick_them_nits_in_term deadline state (params : params) auto orig_assm_ts
    1.28                             orig_t =
    1.29 @@ -198,9 +210,9 @@
    1.30      (* string -> unit *)
    1.31      val print = pprint o curry Pretty.blk 0 o pstrs
    1.32      (* (unit -> string) -> unit *)
    1.33 -    fun print_m f = pprint_m (curry Pretty.blk 0 o pstrs o f)
    1.34 -    fun print_v f = pprint_v (curry Pretty.blk 0 o pstrs o f)
    1.35 -    fun print_d f = pprint_d (curry Pretty.blk 0 o pstrs o f)
    1.36 +    val print_m = pprint_m o K o plazy
    1.37 +    val print_v = pprint_v o K o plazy
    1.38 +    val print_d = pprint_d o K o plazy
    1.39  
    1.40      (* unit -> unit *)
    1.41      fun check_deadline () =
    1.42 @@ -631,15 +643,7 @@
    1.43            case Kodkod.solve_any_problem overlord deadline max_threads
    1.44                                          max_solutions (map fst problems) of
    1.45              Kodkod.NotInstalled =>
    1.46 -            (print_m (fn () =>
    1.47 -                         "Nitpick requires the external Java program Kodkodi. \
    1.48 -                         \To install it, download the package from Isabelle's \
    1.49 -                         \web page and add the \"kodkodi-x.y.z\" directory's \
    1.50 -                         \full path to \"" ^
    1.51 -                         Path.implode (Path.expand (Path.appends
    1.52 -                             (Path.variable "ISABELLE_HOME" ::
    1.53 -                              (map Path.basic ["etc", "components"])))) ^
    1.54 -                         "\".");
    1.55 +            (print_m install_kodkodi_message;
    1.56               (max_potential, max_genuine, donno + 1))
    1.57            | Kodkod.Normal ([], unsat_js) =>
    1.58              (update_checked_problems problems unsat_js;
    1.59 @@ -842,16 +846,21 @@
    1.60  (* Proof.state -> params -> bool -> term -> string * Proof.state *)
    1.61  fun pick_nits_in_term state (params as {debug, timeout, expect, ...})
    1.62                        auto orig_assm_ts orig_t =
    1.63 -  let
    1.64 -    val deadline = Option.map (curry Time.+ (Time.now ())) timeout
    1.65 -    val outcome as (outcome_code, _) =
    1.66 -      time_limit (if debug then NONE else timeout)
    1.67 -          (pick_them_nits_in_term deadline state params auto orig_assm_ts)
    1.68 -          orig_t
    1.69 -  in
    1.70 -    if expect = "" orelse outcome_code = expect then outcome
    1.71 -    else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
    1.72 -  end
    1.73 +  if getenv "KODKODI" = "" then
    1.74 +    (if auto then ()
    1.75 +     else warning (Pretty.string_of (plazy install_kodkodi_message));
    1.76 +     ("unknown", state))
    1.77 +  else
    1.78 +    let
    1.79 +      val deadline = Option.map (curry Time.+ (Time.now ())) timeout
    1.80 +      val outcome as (outcome_code, _) =
    1.81 +        time_limit (if debug then NONE else timeout)
    1.82 +            (pick_them_nits_in_term deadline state params auto orig_assm_ts)
    1.83 +            orig_t
    1.84 +    in
    1.85 +      if expect = "" orelse outcome_code = expect then outcome
    1.86 +      else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
    1.87 +    end
    1.88  
    1.89  (* Proof.state -> params -> thm -> int -> string * Proof.state *)
    1.90  fun pick_nits_in_subgoal state params auto subgoal =