# HG changeset patch
# User wenzelm
# Date 1601041433 -7200
# Node ID 0c7a74a1c6d994b16a47aa96d8597c507b7fbe57
# Parent  a540283d6b58da1c04f8de91ed80fbf99bc31b5e
clarified defaults for nitpick;

diff -r a540283d6b58 -r 0c7a74a1c6d9 NEWS
--- a/NEWS	Fri Sep 25 15:40:35 2020 +0200
+++ b/NEWS	Fri Sep 25 15:43:53 2020 +0200
@@ -16,6 +16,9 @@
 
 *** Isabelle/jEdit Prover IDE ***
 
+* Auto nitpick is enabled by default: it is now reasonably fast due to
+Kodkod invocation within Isabelle/Scala.
+
 * The jEdit status line includes widgets both for JVM and ML heap usage.
 Ongoing ML ongoing garbage collection is shown as "ML cleanup".
 
@@ -50,7 +53,7 @@
 * Nitpick/Kodkod may be invoked directly within the running
 Isabelle/Scala session (instead of an external Java process): this
 improves reactivity and saves resources. This experimental feature is
-guarded by system option "kodkod_scala" (default: false).
+guarded by system option "kodkod_scala" (default: true).
 
 * Session HOL-Examples contains notable examples for Isabelle/HOL
 (former entries of HOL-Isar_Examples, HOL-ex etc.).
diff -r a540283d6b58 -r 0c7a74a1c6d9 src/HOL/Tools/etc/options
--- a/src/HOL/Tools/etc/options	Fri Sep 25 15:40:35 2020 +0200
+++ b/src/HOL/Tools/etc/options	Fri Sep 25 15:43:53 2020 +0200
@@ -8,7 +8,7 @@
 public option auto_time_limit : real = 2.0
   -- "time limit for automatically tried tools (seconds > 0)"
 
-public option auto_nitpick : bool = false
+public option auto_nitpick : bool = true
   -- "run Nitpick automatically"
 
 public option auto_sledgehammer : bool = false
@@ -38,7 +38,7 @@
 public option MaSh : string = "sml"
   -- "machine learning algorithm to use by Sledgehammer (nb_knn, nb, knn, none)"
 
-public option kodkod_scala : bool = false
+public option kodkod_scala : bool = true
   -- "invoke Nitpick/Kodkod via Isabelle/Scala (instead of external process)"
 
 public option kodkod_max_threads : int = 0