# HG changeset patch
# User wenzelm
# Date 1614625473 -3600
# Node ID 5c0e23d73cea317f15e278736a80f6835485652b
# Parent  0af9e7e4476ff9e439df06b6e0565a998a87487b
tuned --- fewer warnings;

diff -r 0af9e7e4476f -r 5c0e23d73cea src/HOL/Tools/Nitpick/kodkod.scala
--- a/src/HOL/Tools/Nitpick/kodkod.scala	Mon Mar 01 19:41:52 2021 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.scala	Mon Mar 01 20:04:33 2021 +0100
@@ -60,35 +60,37 @@
 
     class Exit extends Exception("EXIT")
 
-    val context =
-      new Context {
-        private var rc = 0
-        private val out = new StringBuilder
-        private val err = new StringBuilder
+    class Exec_Context extends 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}
 
-        def return_code(i: Int): Unit = synchronized { rc = rc max i}
+      override def output(s: String): Unit = synchronized {
+        Exn.Interrupt.expose()
+        out ++= s
+        out += '\n'
+      }
 
-        override def output(s: String): Unit = synchronized {
-          Exn.Interrupt.expose()
-          out ++= s
-          out += '\n'
+      override def error(s: String): Unit = synchronized {
+        Exn.Interrupt.expose()
+        err ++= s
+        err += '\n'
+      }
+
+      override def exit(i: Int): Unit =
+        synchronized {
+          return_code(i)
+          executor_kill()
+          throw new Exit
         }
 
-        override def error(s: String): Unit = synchronized {
-          Exn.Interrupt.expose()
-          err ++= s
-          err += '\n'
-        }
+      def result(): Result = synchronized { Result(rc, out.toString, err.toString) }
+    }
 
-        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) }
-      }
+    val context = new Exec_Context
 
 
     /* main */