src/HOL/Tools/Nitpick/kodkod.scala
changeset 75393 87ebf5a50283
parent 74486 74a36aae067a
child 78243 0e221a8128e4
--- a/src/HOL/Tools/Nitpick/kodkod.scala	Fri Apr 01 11:51:42 2022 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.scala	Fri Apr 01 17:06:10 2022 +0200
@@ -14,18 +14,15 @@
 import isabelle.kodkodi.{Context, KodkodiLexer, KodkodiParser}
 
 
-object Kodkod
-{
+object Kodkod {
   /** result **/
 
-  sealed case class Result(rc: Int, out: String, err: String)
-  {
+  sealed case class Result(rc: Int, out: String, err: String) {
     def ok: Boolean = rc == Process_Result.RC.ok
     def check: String =
       if (ok) out else error(if (err.isEmpty) "Error" else err)
 
-    def encode: XML.Body =
-    {
+    def encode: XML.Body = {
       import XML.Encode._
       triple(int, string, string)((rc, out, err))
     }
@@ -41,8 +38,8 @@
     max_solutions: Int = Integer.MAX_VALUE,
     cleanup_inst: Boolean = false,
     timeout: Time = Time.zero,
-    max_threads: Int = 0): Result =
-  {
+    max_threads: Int = 0
+  ): Result = {
     /* executor */
 
     val pool_size = if (max_threads == 0) Isabelle_Thread.max_threads() else max_threads
@@ -60,8 +57,7 @@
 
     class Exit extends Exception("EXIT")
 
-    class Exec_Context extends Context
-    {
+    class Exec_Context extends Context {
       private var rc = Process_Result.RC.ok
       private val out = new StringBuilder
       private val err = new StringBuilder
@@ -145,8 +141,7 @@
       "solver: \"MiniSat\"\n" +
       File.read(Path.explode("$KODKODI/examples/weber3.kki"))).check
 
-  class Handler extends Session.Protocol_Handler
-  {
+  class Handler extends Session.Protocol_Handler {
     override def init(session: Session): Unit = warmup()
   }
 
@@ -154,13 +149,10 @@
 
   /** scala function **/
 
-  object Fun extends Scala.Fun_String("kodkod", thread = true)
-  {
+  object Fun extends Scala.Fun_String("kodkod", thread = true) {
     val here = Scala_Project.here
-    def apply(args: String): String =
-    {
-      val (timeout, (solve_all, (max_solutions, (max_threads, kki)))) =
-      {
+    def apply(args: String): String = {
+      val (timeout, (solve_all, (max_solutions, (max_threads, kki)))) = {
         import XML.Decode._
         pair(int, pair(bool, pair(int, pair(int, string))))(YXML.parse_body(args))
       }