src/HOL/Tools/Nitpick/kodkod.ML
changeset 72330 562445121de7
parent 72329 6255e532aa36
child 72333 0823524eea1e
equal deleted inserted replaced
72329:6255e532aa36 72330:562445121de7
  1052             perhaps (try (unprefix "Solve error: ")) #>
  1052             perhaps (try (unprefix "Solve error: ")) #>
  1053             perhaps (try (unprefix "Error: ")))
  1053             perhaps (try (unprefix "Error: ")))
  1054           |> find_first (fn line => line <> "" andalso line <> "EXIT")
  1054           |> find_first (fn line => line <> "" andalso line <> "EXIT")
  1055           |> the_default ""
  1055           |> the_default ""
  1056       in
  1056       in
  1057         if null ps then
  1057         if not (null ps) orelse rc = 0 then Normal (ps, js, first_error)
  1058           if rc = 130 then
  1058         else if rc = 2 then TimedOut js
  1059             raise Exn.Interrupt
  1059         else if rc = 130 then raise Exn.Interrupt
  1060           else if rc = 2 then
  1060         else Error (if first_error = "" then "Unknown error" else first_error, js)
  1061             TimedOut js
       
  1062           else if rc = 0 then
       
  1063             Normal ([], js, first_error)
       
  1064           else if first_error <> "" then
       
  1065             Error (first_error, js)
       
  1066           else
       
  1067             Error ("Unknown error", js)
       
  1068         else
       
  1069           Normal (ps, js, first_error)
       
  1070       end
  1061       end
  1071   end
  1062   end
  1072 
  1063 
  1073 val cached_outcome =
  1064 val cached_outcome =
  1074   Synchronized.var "Kodkod.cached_outcome"
  1065   Synchronized.var "Kodkod.cached_outcome"