# HG changeset patch
# User wenzelm
# Date 1597836593 -7200
# Node ID fbaa6b40b43973cb306c9f2742d398990f2ffe57
# Parent  22c11f65ddf960f2df0ec51064f226f59558c4c2
update to kodkodi-1.5.4;
more realistic kodkod invocation;

diff -r 22c11f65ddf9 -r fbaa6b40b439 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Tue Aug 18 18:23:17 2020 +0200
+++ b/Admin/components/components.sha1	Wed Aug 19 13:29:53 2020 +0200
@@ -181,6 +181,7 @@
 afb04f4048a87bb888fe7b05b0139cb060c7925b  kodkodi-1.5.2-1.tar.gz
 5f95c96bb99927f3a026050f85bd056f37a9189e  kodkodi-1.5.2.tar.gz
 0634a946b216f7f07f1a0f7e28cf345daa28828f  kodkodi-1.5.3.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 22c11f65ddf9 -r fbaa6b40b439 Admin/components/main
--- a/Admin/components/main	Tue Aug 18 18:23:17 2020 +0200
+++ b/Admin/components/main	Wed Aug 19 13:29:53 2020 +0200
@@ -9,7 +9,7 @@
 jedit_build-20200610
 jfreechart-1.5.0
 jortho-1.0-2
-kodkodi-1.5.3
+kodkodi-1.5.4
 nunchaku-0.5
 opam-2.0.6
 polyml-test-f54aa41240d0
diff -r 22c11f65ddf9 -r fbaa6b40b439 src/HOL/Tools/Nitpick/kodkod.scala
--- a/src/HOL/Tools/Nitpick/kodkod.scala	Tue Aug 18 18:23:17 2020 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.scala	Wed Aug 19 13:29:53 2020 +0200
@@ -8,8 +8,10 @@
 
 import isabelle._
 
+import java.util.concurrent.Executors
+
 import org.antlr.runtime.{ANTLRInputStream, Lexer, RecognitionException}
-import de.tum.in.isabelle.Kodkodi.{KodkodiLexer, KodkodiParser}
+import de.tum.in.isabelle.Kodkodi.{Context, KodkodiLexer, KodkodiParser}
 
 
 object Kodkod
@@ -19,17 +21,40 @@
     prove: Boolean = false,
     max_solutions: Int = Integer.MAX_VALUE,
     cleanup_inst: Boolean = false,
-    time_limit: Time = Time.zero,
     max_threads: Int = 1): String =
   {
-    val in = Bytes(source).stream
-    val stream = new ANTLRInputStream(in)
-    val lexer = new KodkodiLexer(stream)
-
+    val context =
+      new Context {
+        private val out = new StringBuilder
+        private val err = new StringBuilder
+        def result: (String, String) = synchronized { (out.toString, err.toString) }
+        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(rc: Int) { if (rc == 0) () else error("exit " + rc) }
+      }
+    val executor = Executors.newFixedThreadPool(max_threads)
+    val lexer = new KodkodiLexer(new ANTLRInputStream(Bytes(source).stream))
     val parser =
-      KodkodiParser.create(true, false, solve_all, prove, max_solutions,
-        cleanup_inst, max_threads, lexer)
+      KodkodiParser.create(context, executor,
+        false, solve_all, prove, max_solutions, cleanup_inst, lexer)
 
-    "FIXME"
+    val solution =
+        try { parser.problems() }
+        catch {
+          case exn: RecognitionException =>
+            parser.reportError(exn)
+            error("Parser error")
+        }
+    if (parser.getTokenStream.LA(1) != KodkodiParser.EOF) {
+      error("Trailing tokens")
+    }
+    if (lexer.getNumberOfSyntaxErrors > 0) error("Lexical error")
+    if (parser.getNumberOfSyntaxErrors > 0) error("Syntax error")
+
+    val (out, err) = context.result
+    Output.writeln(out)
+    Output.warning(err)
+
+    solution
   }
 }