# HG changeset patch
# User blanchet
# Date 1274971323 -7200
# Node ID f69efa106feb2ad7aa39ebb983df2388ae70c48b
# Parent  fd6308b4df72b47f91a7bbcfc55bd791e83229e8
make Nitpick "show_all" option behave less surprisingly

diff -r fd6308b4df72 -r f69efa106feb doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Thu May 27 15:28:23 2010 +0200
+++ b/doc-src/Nitpick/nitpick.tex	Thu May 27 16:42:03 2010 +0200
@@ -2226,9 +2226,8 @@
 sometimes helpful when investigating why a counterexample is
 genuine, but they can clutter the output.
 
-\opfalse{show\_all}{dont\_show\_all}
-Enabling this option effectively enables \textit{show\_datatypes} and
-\textit{show\_consts}.
+\opnodefault{show\_all}{bool}
+Abbreviation for \textit{show\_datatypes} and \textit{show\_consts}.
 
 \opdefault{max\_potential}{int}{$\mathbf{1}$}
 Specifies the maximum number of potential counterexamples to display. Setting
diff -r fd6308b4df72 -r f69efa106feb src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Thu May 27 15:28:23 2010 +0200
+++ b/src/HOL/Library/Multiset.thy	Thu May 27 16:42:03 2010 +0200
@@ -1699,7 +1699,6 @@
   by (fact multiset_order.less_asym)
 
 ML {*
-(* Proof.context -> string -> (typ -> term list) -> typ -> term -> term *)
 fun multiset_postproc _ maybe_name all_values (T as Type (_, [elem_T]))
                       (Const _ $ t') =
     let
@@ -1727,4 +1726,4 @@
 Nitpick.register_term_postprocessor @{typ "'a multiset"} multiset_postproc
 *}
 
-end
\ No newline at end of file
+end
diff -r fd6308b4df72 -r f69efa106feb src/HOL/Tools/Nitpick/nitpick_isar.ML
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Thu May 27 15:28:23 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Thu May 27 16:42:03 2010 +0200
@@ -62,7 +62,6 @@
    ("debug", "false"),
    ("verbose", "false"),
    ("overlord", "false"),
-   ("show_all", "false"),
    ("show_datatypes", "false"),
    ("show_consts", "false"),
    ("format", "1"),
@@ -91,7 +90,6 @@
    ("no_debug", "debug"),
    ("quiet", "verbose"),
    ("no_overlord", "overlord"),
-   ("dont_show_all", "show_all"),
    ("hide_datatypes", "show_datatypes"),
    ("hide_consts", "show_consts"),
    ("trust_potential", "check_potential"),
@@ -100,7 +98,7 @@
 fun is_known_raw_param s =
   AList.defined (op =) default_default_params s orelse
   AList.defined (op =) negated_params s orelse
-  s = "max" orelse s = "eval" orelse s = "expect" orelse
+  s = "max" orelse s = "show_all" orelse s = "eval" orelse s = "expect" orelse
   exists (fn p => String.isPrefix (p ^ " ") s)
          ["card", "max", "iter", "box", "dont_box", "finitize", "dont_finitize",
           "mono", "non_mono", "std", "non_std", "wf", "non_wf", "format"]
@@ -115,14 +113,17 @@
             else if String.isPrefix "non_" name then SOME (unprefix "non_" name)
             else NONE
   | some_name => some_name
-fun unnegate_raw_param (name, value) =
+fun normalize_raw_param (name, value) =
   case unnegate_param_name name of
-    SOME name' => (name', case value of
-                            ["false"] => ["true"]
-                          | ["true"] => ["false"]
-                          | [] => ["false"]
-                          | _ => value)
-  | NONE => (name, value)
+    SOME name' => [(name', case value of
+                             ["false"] => ["true"]
+                           | ["true"] => ["false"]
+                           | [] => ["false"]
+                           | _ => value)]
+  | NONE => if name = "show_all" then
+              [("show_datatypes", value), ("show_consts", value)]
+            else
+              [(name, value)]
 
 structure Data = Theory_Data(
   type T = raw_param list
@@ -130,7 +131,8 @@
   val extend = I
   fun merge (x, y) = AList.merge (op =) (K true) (x, y))
 
-val set_default_raw_param = Data.map o AList.update (op =) o unnegate_raw_param
+val set_default_raw_param =
+  Data.map o fold (AList.update (op =)) o normalize_raw_param
 val default_raw_params = Data.get
 
 fun is_punctuation s = (s = "," orelse s = "-" orelse s = "\<midarrow>")
@@ -145,7 +147,7 @@
 
 fun extract_params ctxt auto default_params override_params =
   let
-    val override_params = map unnegate_raw_param override_params
+    val override_params = maps normalize_raw_param override_params
     val raw_params = rev override_params @ rev default_params
     val lookup =
       Option.map stringify_raw_param_value o AList.lookup (op =) raw_params
@@ -250,9 +252,8 @@
     val timeout = if auto then NONE else lookup_time "timeout"
     val tac_timeout = lookup_time "tac_timeout"
     val max_threads = Int.max (0, lookup_int "max_threads")
-    val show_all = debug orelse lookup_bool "show_all"
-    val show_datatypes = show_all orelse lookup_bool "show_datatypes"
-    val show_consts = show_all orelse lookup_bool "show_consts"
+    val show_datatypes = debug orelse lookup_bool "show_datatypes"
+    val show_consts = debug orelse lookup_bool "show_consts"
     val formats = lookup_ints_assigns read_term_polymorphic "format" 0
     val evals = lookup_term_list "eval"
     val max_potential =