src/HOL/Tools/Nitpick/nitpick.ML
changeset 72205 bc71db05abe3
parent 72195 16f2288b30cf
child 72298 a540283d6b58
equal deleted inserted replaced
72204:cb746b19e1d7 72205:bc71db05abe3
   174 
   174 
   175 val isabelle_wrong_message =
   175 val isabelle_wrong_message =
   176   "something appears to be wrong with your Isabelle installation"
   176   "something appears to be wrong with your Isabelle installation"
   177 val java_not_found_message =
   177 val java_not_found_message =
   178   "Java could not be launched -- " ^ isabelle_wrong_message
   178   "Java could not be launched -- " ^ isabelle_wrong_message
   179 val java_too_old_message =
       
   180   "The Java version is too old -- " ^ isabelle_wrong_message
       
   181 val kodkodi_not_installed_message =
   179 val kodkodi_not_installed_message =
   182   "Nitpick requires the external Java program Kodkodi"
   180   "Nitpick requires the external Java program Kodkodi"
   183 val kodkodi_too_old_message = "The installed Kodkodi version is too old"
       
   184 
   181 
   185 val max_unsound_delay_ms = 200
   182 val max_unsound_delay_ms = 200
   186 val max_unsound_delay_percent = 2
   183 val max_unsound_delay_percent = 2
   187 
   184 
   188 fun unsound_delay_for_timeout timeout =
   185 fun unsound_delay_for_timeout timeout =
   723           case KK.solve_any_problem debug overlord deadline max_threads
   720           case KK.solve_any_problem debug overlord deadline max_threads
   724                                     max_solutions (map fst problems) of
   721                                     max_solutions (map fst problems) of
   725             KK.JavaNotFound =>
   722             KK.JavaNotFound =>
   726             (print_nt (K java_not_found_message);
   723             (print_nt (K java_not_found_message);
   727              (found_really_genuine, max_potential, max_genuine, donno + 1))
   724              (found_really_genuine, max_potential, max_genuine, donno + 1))
   728           | KK.JavaTooOld =>
       
   729             (print_nt (K java_too_old_message);
       
   730              (found_really_genuine, max_potential, max_genuine, donno + 1))
       
   731           | KK.KodkodiNotInstalled =>
   725           | KK.KodkodiNotInstalled =>
   732             (print_nt (K kodkodi_not_installed_message);
   726             (print_nt (K kodkodi_not_installed_message);
   733              (found_really_genuine, max_potential, max_genuine, donno + 1))
       
   734           | KK.KodkodiTooOld =>
       
   735             (print_nt (K kodkodi_too_old_message);
       
   736              (found_really_genuine, max_potential, max_genuine, donno + 1))
   727              (found_really_genuine, max_potential, max_genuine, donno + 1))
   737           | KK.Normal ([], unsat_js, s) =>
   728           | KK.Normal ([], unsat_js, s) =>
   738             (update_checked_problems problems unsat_js; show_kodkod_warning s;
   729             (update_checked_problems problems unsat_js; show_kodkod_warning s;
   739              (found_really_genuine, max_potential, max_genuine, donno))
   730              (found_really_genuine, max_potential, max_genuine, donno))
   740           | KK.Normal (sat_ps, unsat_js, s) =>
   731           | KK.Normal (sat_ps, unsat_js, s) =>