--- a/src/HOL/Tools/Nitpick/kodkod.ML Mon Aug 24 21:47:21 2020 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Mon Aug 24 22:30:34 2020 +0200
@@ -1057,11 +1057,12 @@
val first_error =
trim_split_lines err
- |> find_first (fn line => line <> "")
+ |> map
+ (perhaps (try (unsuffix ".")) #>
+ perhaps (try (unprefix "Solve error: ")) #>
+ perhaps (try (unprefix "Error: ")))
+ |> find_first (fn line => line <> "" andalso line <> "EXIT")
|> the_default ""
- |> perhaps (try (unsuffix "."))
- |> perhaps (try (unprefix "Solve error: "))
- |> perhaps (try (unprefix "Error: "))
fun has_error s =
first_error |> Substring.full |> Substring.position s |> snd
|> Substring.isEmpty |> not