src/HOL/Tools/Nitpick/nitpick.ML
changeset 49024 224a0c63ba23
parent 48323 7b5f7ca25d17
child 49358 0fa351b1bd14
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Thu Aug 30 09:47:46 2012 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Thu Aug 30 09:47:46 2012 +0200
     1.3 @@ -179,9 +179,13 @@
     1.4                                   Pretty.str (if j = 1 then "." else ";")])
     1.5                 (length ts downto 1) ts))]
     1.6  
     1.7 -fun install_java_message () =
     1.8 -  "Nitpick requires Java Development Kit 1.6 via ISABELLE_JDK_HOME setting."
     1.9 -fun install_kodkodi_message () =
    1.10 +val isabelle_wrong_message =
    1.11 +  "Something appears to be wrong with your Isabelle installation."
    1.12 +fun java_not_found_message () =
    1.13 +  "Java could not be launched. " ^ isabelle_wrong_message
    1.14 +fun java_too_old_message () =
    1.15 +  "The Java version is too old. " ^ isabelle_wrong_message
    1.16 +fun kodkodi_not_installed_message () =
    1.17    "Nitpick requires the external Java program Kodkodi. To install it, download \
    1.18    \the package from \"http://www21.in.tum.de/~blanchet/#software\" and add the \
    1.19    \\"kodkodi-x.y.z\" directory's full path to " ^
    1.20 @@ -802,14 +806,14 @@
    1.21          else
    1.22            case KK.solve_any_problem debug overlord deadline max_threads
    1.23                                      max_solutions (map fst problems) of
    1.24 -            KK.JavaNotInstalled =>
    1.25 -            (print_nt install_java_message;
    1.26 +            KK.JavaNotFound =>
    1.27 +            (print_nt java_not_found_message;
    1.28               (found_really_genuine, max_potential, max_genuine, donno + 1))
    1.29            | KK.JavaTooOld =>
    1.30 -            (print_nt install_java_message;
    1.31 +            (print_nt java_too_old_message;
    1.32               (found_really_genuine, max_potential, max_genuine, donno + 1))
    1.33            | KK.KodkodiNotInstalled =>
    1.34 -            (print_nt install_kodkodi_message;
    1.35 +            (print_nt kodkodi_not_installed_message;
    1.36               (found_really_genuine, max_potential, max_genuine, donno + 1))
    1.37            | KK.Normal ([], unsat_js, s) =>
    1.38              (update_checked_problems problems unsat_js; show_kodkod_warning s;
    1.39 @@ -1062,7 +1066,7 @@
    1.40      if getenv "KODKODI" = "" then
    1.41        (* The "expect" argument is deliberately ignored if Kodkodi is missing so
    1.42           that the "Nitpick_Examples" can be processed on any machine. *)
    1.43 -      (print_nt (Pretty.string_of (plazy install_kodkodi_message));
    1.44 +      (print_nt (Pretty.string_of (plazy kodkodi_not_installed_message));
    1.45         ("no_kodkodi", state))
    1.46      else
    1.47        let