# HG changeset patch
# User wenzelm
# Date 1597926169 -7200
# Node ID 0841895ca438cc4b73576ef47493d7fd802d3058
# Parent  2481cdb8483292a1a00b0e3e1aff36aad53b1b81
clarified signature;

diff -r 2481cdb84832 -r 0841895ca438 src/HOL/Tools/Nitpick/kodkod.scala
--- a/src/HOL/Tools/Nitpick/kodkod.scala	Wed Aug 19 20:14:41 2020 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.scala	Thu Aug 20 14:22:49 2020 +0200
@@ -17,8 +17,13 @@
 object Kodkod
 {
   sealed case class Result(rc: Int, out: String, err: String)
+  {
+    def ok: Boolean = rc == 0
+    def check: String =
+      if (ok) out else error(if (err.isEmpty) "Error" else err)
+  }
 
-  def kodkod(source: String,
+  def execute(source: String,
     solve_all: Boolean = false,
     prove: Boolean = false,
     max_solutions: Int = Integer.MAX_VALUE,
@@ -91,4 +96,7 @@
 
     context.result()
   }
+
+  def warmup(): String =
+    execute(File.read(Path.explode("$KODKODI/examples/weber3.kki"))).check
 }