# HG changeset patch
# User wenzelm
# Date 1598301034 -7200
# Node ID 733bab4c1be004f56dfa86ed00a2a63d6034fc22
# Parent  0840240dfb24a5127b6fcf18df896c6bad111f84
suppress odd warning for context.exit();

diff -r 0840240dfb24 -r 733bab4c1be0 src/HOL/Tools/Nitpick/kodkod.ML
--- 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
diff -r 0840240dfb24 -r 733bab4c1be0 src/HOL/Tools/Nitpick/kodkod.scala
--- a/src/HOL/Tools/Nitpick/kodkod.scala	Mon Aug 24 21:47:21 2020 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.scala	Mon Aug 24 22:30:34 2020 +0200
@@ -43,7 +43,7 @@
     def executor_kill(): Unit =
       if (!executor.isShutdown) Isabelle_Thread.fork() { executor.shutdownNow() }
 
-    class Exit extends Exception
+    class Exit extends Exception("EXIT")
 
     val context =
       new Context {