# HG changeset patch
# User wenzelm
# Date 1597932059 -7200
# Node ID 1337904169d7f54edceac4c6c28c452c5af3a428
# Parent  585b877df6986b30950e31c0654bd8e74fd44cbd# Parent  6241cbbf5a5827e87dfc2cc5a0e84abf71e1936d
merged

diff -r 585b877df698 -r 1337904169d7 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Thu Aug 20 11:52:46 2020 +0200
+++ b/Admin/components/components.sha1	Thu Aug 20 16:00:59 2020 +0200
@@ -180,6 +180,9 @@
 6c737137cc597fc920943783382e928ea79e3feb  kodkodi-1.2.16.tar.gz
 afb04f4048a87bb888fe7b05b0139cb060c7925b  kodkodi-1.5.2-1.tar.gz
 5f95c96bb99927f3a026050f85bd056f37a9189e  kodkodi-1.5.2.tar.gz
+0634a946b216f7f07f1a0f7e28cf345daa28828f  kodkodi-1.5.3.tar.gz
+52e95b3493d71902f9df89d0bb59d0046a5f0c63  kodkodi-1.5.4-1.tar.gz
+267189c637de26cf304d699cfa95389da002b250  kodkodi-1.5.4.tar.gz
 377e36efb8608e6c828c7718d890e97fde2006a4  linux_app-20131007.tar.gz
 759848095e2ad506083d92b5646947e3c32f27a0  linux_app-20191223.tar.gz
 1a449ce69ac874e21804595d16aaaf5a0d0d0c10  linux_app-20200110.tar.gz
diff -r 585b877df698 -r 1337904169d7 Admin/components/main
--- a/Admin/components/main	Thu Aug 20 11:52:46 2020 +0200
+++ b/Admin/components/main	Thu Aug 20 16:00:59 2020 +0200
@@ -9,7 +9,7 @@
 jedit_build-20200610
 jfreechart-1.5.0
 jortho-1.0-2
-kodkodi-1.5.2-1
+kodkodi-1.5.4-1
 nunchaku-0.5
 opam-2.0.6
 polyml-test-f54aa41240d0
diff -r 585b877df698 -r 1337904169d7 src/HOL/Tools/Nitpick/kodkod.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Nitpick/kodkod.scala	Thu Aug 20 16:00:59 2020 +0200
@@ -0,0 +1,104 @@
+/*  Title:      HOL/Tools/Nitpick/kodkod.scala
+    Author:     Makarius
+
+Scala interface for Kodkod.
+*/
+
+package isabelle.nitpick
+
+import isabelle._
+
+import java.util.concurrent.Executors
+
+import org.antlr.runtime.{ANTLRInputStream, RecognitionException}
+import de.tum.in.isabelle.Kodkodi.{Context, KodkodiLexer, KodkodiParser}
+
+
+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 execute(source: String,
+    solve_all: Boolean = false,
+    prove: Boolean = false,
+    max_solutions: Int = Integer.MAX_VALUE,
+    cleanup_inst: Boolean = false,
+    timeout: Time = Time.zero,
+    max_threads: Int = 1): Result =
+  {
+    val executor = Executors.newFixedThreadPool(max_threads)
+
+    def executor_kill(): Unit =
+      if (!executor.isShutdown) Isabelle_Thread.fork() { executor.shutdownNow() }
+
+    class Exit extends Exception
+
+    val context =
+      new Context {
+        private var rc = 0
+        private val out = new StringBuilder
+        private val err = new StringBuilder
+
+        def return_code(i: Int): Unit = synchronized { rc = rc max i}
+        override def output(s: String): Unit = synchronized { out ++= s; out += '\n' }
+        override def error(s: String): Unit = synchronized { err ++= s; err += '\n' }
+        override def exit(i: Int): Unit =
+          synchronized {
+            return_code(i)
+            executor_kill()
+            throw new Exit
+          }
+
+        def result(): Result = synchronized { Result(rc, out.toString, err.toString) }
+      }
+
+    try {
+      val lexer = new KodkodiLexer(new ANTLRInputStream(Bytes(source).stream))
+      val parser =
+        KodkodiParser.create(context, executor,
+          false, solve_all, prove, max_solutions, cleanup_inst, lexer)
+
+      val timeout_request =
+        if (timeout.is_zero) None
+        else {
+          Some(Event_Timer.request(Time.now() + timeout) {
+            context.error("Ran out of time")
+            context.return_code(2)
+            executor_kill()
+          })
+        }
+
+      try { parser.problems() }
+      catch { case exn: RecognitionException => parser.reportError(exn) }
+
+      timeout_request.foreach(_.cancel)
+
+      if (parser.getTokenStream.LA(1) != KodkodiParser.EOF) {
+        context.error("Error: trailing tokens")
+        context.exit(1)
+      }
+      if (lexer.getNumberOfSyntaxErrors + parser.getNumberOfSyntaxErrors > 0) {
+        context.exit(1)
+      }
+    }
+    catch {
+      case _: Exit =>
+      case exn: Throwable =>
+        val message = exn.getMessage
+        context.error(if (message.isEmpty) exn.toString else "Error: " + message)
+        context.return_code(1)
+    }
+
+    context.result()
+  }
+
+  def warmup(): String =
+    execute(
+      """solver: "MiniSat\n"""" +
+      File.read(Path.explode("$KODKODI/examples/weber3.kki"))).check
+}
diff -r 585b877df698 -r 1337904169d7 src/Pure/Tools/scala_project.scala
--- a/src/Pure/Tools/scala_project.scala	Thu Aug 20 11:52:46 2020 +0200
+++ b/src/Pure/Tools/scala_project.scala	Thu Aug 20 16:00:59 2020 +0200
@@ -57,7 +57,8 @@
       "src/Tools/Graphview/" -> Path.explode("isabelle.graphview"),
       "src/Tools/VSCode/" -> Path.explode("isabelle.vscode"),
       "src/Tools/jEdit/src-base/" -> Path.explode("isabelle.jedit_base"),
-      "src/Tools/jEdit/src/" -> Path.explode("isabelle.jedit"))
+      "src/Tools/jEdit/src/" -> Path.explode("isabelle.jedit"),
+      "src/HOL/Tools/Nitpick" -> Path.explode("isabelle.nitpick"))
 
 
   /* scala project */
diff -r 585b877df698 -r 1337904169d7 src/Pure/build-jars
--- a/src/Pure/build-jars	Thu Aug 20 11:52:46 2020 +0200
+++ b/src/Pure/build-jars	Thu Aug 20 16:00:59 2020 +0200
@@ -9,6 +9,7 @@
 ## sources
 
 declare -a SOURCES=(
+  src/HOL/Tools/Nitpick/kodkod.scala
   src/Pure/Admin/afp.scala
   src/Pure/Admin/build_cygwin.scala
   src/Pure/Admin/build_doc.scala