suppress odd warning for context.exit();
authorwenzelm
Mon, 24 Aug 2020 22:30:34 +0200
changeset 72203 733bab4c1be0
parent 72202 0840240dfb24
child 72204 cb746b19e1d7
suppress odd warning for context.exit();
src/HOL/Tools/Nitpick/kodkod.ML
src/HOL/Tools/Nitpick/kodkod.scala
--- 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
--- 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 {