# HG changeset patch
# User wenzelm
# Date 1597767797 -7200
# Node ID 22c11f65ddf960f2df0ec51064f226f59558c4c2
# Parent  6d7cd8e7bc6de2da3d4ab7656dee0a8156991fb6
rudiments of Scala interface for Kodkod;

diff -r 6d7cd8e7bc6d -r 22c11f65ddf9 src/HOL/Tools/Nitpick/kodkod.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Nitpick/kodkod.scala	Tue Aug 18 18:23:17 2020 +0200
@@ -0,0 +1,35 @@
+/*  Title:      HOL/Tools/Nitpick/kodkod.scala
+    Author:     Makarius
+
+Scala interface for Kodkod.
+*/
+
+package isabelle.nitpick
+
+import isabelle._
+
+import org.antlr.runtime.{ANTLRInputStream, Lexer, RecognitionException}
+import de.tum.in.isabelle.Kodkodi.{KodkodiLexer, KodkodiParser}
+
+
+object Kodkod
+{
+  def kodkod(source: String,
+    solve_all: Boolean = false,
+    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 parser =
+      KodkodiParser.create(true, false, solve_all, prove, max_solutions,
+        cleanup_inst, max_threads, lexer)
+
+    "FIXME"
+  }
+}
diff -r 6d7cd8e7bc6d -r 22c11f65ddf9 src/Pure/Tools/scala_project.scala
--- a/src/Pure/Tools/scala_project.scala	Tue Aug 18 17:58:35 2020 +0200
+++ b/src/Pure/Tools/scala_project.scala	Tue Aug 18 18:23:17 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 6d7cd8e7bc6d -r 22c11f65ddf9 src/Pure/build-jars
--- a/src/Pure/build-jars	Tue Aug 18 17:58:35 2020 +0200
+++ b/src/Pure/build-jars	Tue Aug 18 18:23:17 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