--- /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"
+ }
+}
--- 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 */
--- 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