updated Java-related error message
authorblanchet
Thu Aug 30 09:47:46 2012 +0200 (2012-08-30 ago)
changeset 49024224a0c63ba23
parent 49023 5afe918dd476
child 49025 7e89b0520e83
updated Java-related error message
src/HOL/Tools/Nitpick/kodkod.ML
src/HOL/Tools/Nitpick/nitpick.ML
     1.1 --- a/src/HOL/Tools/Nitpick/kodkod.ML	Thu Aug 30 09:47:46 2012 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/kodkod.ML	Thu Aug 30 09:47:46 2012 +0200
     1.3 @@ -155,7 +155,7 @@
     1.4    type raw_bound = n_ary_index * int list list
     1.5  
     1.6    datatype outcome =
     1.7 -    JavaNotInstalled |
     1.8 +    JavaNotFound |
     1.9      JavaTooOld |
    1.10      KodkodiNotInstalled |
    1.11      Normal of (int * raw_bound list) list * int list * string |
    1.12 @@ -302,7 +302,7 @@
    1.13  type raw_bound = n_ary_index * int list list
    1.14  
    1.15  datatype outcome =
    1.16 -  JavaNotInstalled |
    1.17 +  JavaNotFound |
    1.18    JavaTooOld |
    1.19    KodkodiNotInstalled |
    1.20    Normal of (int * raw_bound list) list * int list * string |
    1.21 @@ -1068,7 +1068,7 @@
    1.22                  else if code = 0 then
    1.23                    Normal ([], js, first_error)
    1.24                  else if code = 127 then
    1.25 -                  JavaNotInstalled
    1.26 +                  JavaNotFound
    1.27                  else if has_error "UnsupportedClassVersionError" then
    1.28                    JavaTooOld
    1.29                  else if has_error "NoClassDefFoundError" then
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Thu Aug 30 09:47:46 2012 +0200
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Thu Aug 30 09:47:46 2012 +0200
     2.3 @@ -179,9 +179,13 @@
     2.4                                   Pretty.str (if j = 1 then "." else ";")])
     2.5                 (length ts downto 1) ts))]
     2.6  
     2.7 -fun install_java_message () =
     2.8 -  "Nitpick requires Java Development Kit 1.6 via ISABELLE_JDK_HOME setting."
     2.9 -fun install_kodkodi_message () =
    2.10 +val isabelle_wrong_message =
    2.11 +  "Something appears to be wrong with your Isabelle installation."
    2.12 +fun java_not_found_message () =
    2.13 +  "Java could not be launched. " ^ isabelle_wrong_message
    2.14 +fun java_too_old_message () =
    2.15 +  "The Java version is too old. " ^ isabelle_wrong_message
    2.16 +fun kodkodi_not_installed_message () =
    2.17    "Nitpick requires the external Java program Kodkodi. To install it, download \
    2.18    \the package from \"http://www21.in.tum.de/~blanchet/#software\" and add the \
    2.19    \\"kodkodi-x.y.z\" directory's full path to " ^
    2.20 @@ -802,14 +806,14 @@
    2.21          else
    2.22            case KK.solve_any_problem debug overlord deadline max_threads
    2.23                                      max_solutions (map fst problems) of
    2.24 -            KK.JavaNotInstalled =>
    2.25 -            (print_nt install_java_message;
    2.26 +            KK.JavaNotFound =>
    2.27 +            (print_nt java_not_found_message;
    2.28               (found_really_genuine, max_potential, max_genuine, donno + 1))
    2.29            | KK.JavaTooOld =>
    2.30 -            (print_nt install_java_message;
    2.31 +            (print_nt java_too_old_message;
    2.32               (found_really_genuine, max_potential, max_genuine, donno + 1))
    2.33            | KK.KodkodiNotInstalled =>
    2.34 -            (print_nt install_kodkodi_message;
    2.35 +            (print_nt kodkodi_not_installed_message;
    2.36               (found_really_genuine, max_potential, max_genuine, donno + 1))
    2.37            | KK.Normal ([], unsat_js, s) =>
    2.38              (update_checked_problems problems unsat_js; show_kodkod_warning s;
    2.39 @@ -1062,7 +1066,7 @@
    2.40      if getenv "KODKODI" = "" then
    2.41        (* The "expect" argument is deliberately ignored if Kodkodi is missing so
    2.42           that the "Nitpick_Examples" can be processed on any machine. *)
    2.43 -      (print_nt (Pretty.string_of (plazy install_kodkodi_message));
    2.44 +      (print_nt (Pretty.string_of (plazy kodkodi_not_installed_message));
    2.45         ("no_kodkodi", state))
    2.46      else
    2.47        let