# HG changeset patch
# User blanchet
# Date 1284402084 -7200
# Node ID 9de74cdcd833c7e3d00f5f2a01657d55d89369be
# Parent  eac5f82eefb6e379bad4832f6130a69018c67cdd
make Auto Nitpick go through fewer scopes

diff -r eac5f82eefb6 -r 9de74cdcd833 src/HOL/Tools/Nitpick/nitpick_isar.ML
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Mon Sep 13 20:15:04 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Mon Sep 13 20:21:24 2010 +0200
@@ -26,6 +26,10 @@
 
 val auto = Unsynchronized.ref false
 
+(* Maximum number of scopes for Auto Nitpick. Be frugal since it has to share
+   its time slot with several other automatic tools. *)
+val max_auto_scopes = 6
+
 val _ =
   ProofGeneralPgip.add_preference Preferences.category_tracing
       (Preferences.bool_pref auto "auto-nitpick"
@@ -223,6 +227,7 @@
       AList.lookup (op =) raw_params #> these #> map read_term_polymorphic
     val read_const_polymorphic = read_term_polymorphic #> dest_Const
     val cards_assigns = lookup_ints_assigns read_type_polymorphic "card" 1
+                        |> auto ? map (apsnd (take max_auto_scopes))
     val maxes_assigns = lookup_ints_assigns read_const_polymorphic "max" ~1
     val iters_assigns = lookup_ints_assigns read_const_polymorphic "iter" 0
     val bitss = lookup_int_seq "bits" 1