1.1 --- a/doc-src/Nitpick/nitpick.tex	Thu May 27 15:28:23 2010 +0200
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Thu May 27 16:42:03 2010 +0200
     1.3 @@ -2226,9 +2226,8 @@
     1.4  sometimes helpful when investigating why a counterexample is
     1.5  genuine, but they can clutter the output.
     1.6  
     1.7 -\opfalse{show\_all}{dont\_show\_all}
     1.8 -Enabling this option effectively enables \textit{show\_datatypes} and
     1.9 -\textit{show\_consts}.
    1.10 +\opnodefault{show\_all}{bool}
    1.11 +Abbreviation for \textit{show\_datatypes} and \textit{show\_consts}.
    1.12  
    1.13  \opdefault{max\_potential}{int}{$\mathbf{1}$}
    1.14  Specifies the maximum number of potential counterexamples to display. Setting

     2.1 --- a/src/HOL/Library/Multiset.thy	Thu May 27 15:28:23 2010 +0200
     2.2 +++ b/src/HOL/Library/Multiset.thy	Thu May 27 16:42:03 2010 +0200
     2.3 @@ -1699,7 +1699,6 @@
     2.4    by (fact multiset_order.less_asym)
     2.5  
     2.6  ML {*
     2.7 -(* Proof.context -> string -> (typ -> term list) -> typ -> term -> term *)
     2.8  fun multiset_postproc _ maybe_name all_values (T as Type (_, [elem_T]))
     2.9                        (Const _ $ t') =
    2.10      let
    2.11 @@ -1727,4 +1726,4 @@
    2.12  Nitpick.register_term_postprocessor @{typ "'a multiset"} multiset_postproc
    2.13  *}
    2.14  
    2.15 -end
    2.16 \ No newline at end of file
    2.17 +end

     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Thu May 27 15:28:23 2010 +0200
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Thu May 27 16:42:03 2010 +0200
     3.3 @@ -62,7 +62,6 @@
     3.4     ("debug", "false"),
     3.5     ("verbose", "false"),
     3.6     ("overlord", "false"),
     3.7 -   ("show_all", "false"),
     3.8     ("show_datatypes", "false"),
     3.9     ("show_consts", "false"),
    3.10     ("format", "1"),
    3.11 @@ -91,7 +90,6 @@
    3.12     ("no_debug", "debug"),
    3.13     ("quiet", "verbose"),
    3.14     ("no_overlord", "overlord"),
    3.15 -   ("dont_show_all", "show_all"),
    3.16     ("hide_datatypes", "show_datatypes"),
    3.17     ("hide_consts", "show_consts"),
    3.18     ("trust_potential", "check_potential"),
    3.19 @@ -100,7 +98,7 @@
    3.20  fun is_known_raw_param s =
    3.21    AList.defined (op =) default_default_params s orelse
    3.22    AList.defined (op =) negated_params s orelse
    3.23 -  s = "max" orelse s = "eval" orelse s = "expect" orelse
    3.24 +  s = "max" orelse s = "show_all" orelse s = "eval" orelse s = "expect" orelse
    3.25    exists (fn p => String.isPrefix (p ^ " ") s)
    3.26           ["card", "max", "iter", "box", "dont_box", "finitize", "dont_finitize",
    3.27            "mono", "non_mono", "std", "non_std", "wf", "non_wf", "format"]
    3.28 @@ -115,14 +113,17 @@
    3.29              else if String.isPrefix "non_" name then SOME (unprefix "non_" name)
    3.30              else NONE
    3.31    | some_name => some_name
    3.32 -fun unnegate_raw_param (name, value) =
    3.33 +fun normalize_raw_param (name, value) =
    3.34    case unnegate_param_name name of
    3.35 -    SOME name' => (name', case value of
    3.36 -                            ["false"] => ["true"]
    3.37 -                          | ["true"] => ["false"]
    3.38 -                          | [] => ["false"]
    3.39 -                          | _ => value)
    3.40 -  | NONE => (name, value)
    3.41 +    SOME name' => [(name', case value of
    3.42 +                             ["false"] => ["true"]
    3.43 +                           | ["true"] => ["false"]
    3.44 +                           | [] => ["false"]
    3.45 +                           | _ => value)]
    3.46 +  | NONE => if name = "show_all" then
    3.47 +              [("show_datatypes", value), ("show_consts", value)]
    3.48 +            else
    3.49 +              [(name, value)]
    3.50  
    3.51  structure Data = Theory_Data(
    3.52    type T = raw_param list
    3.53 @@ -130,7 +131,8 @@
    3.54    val extend = I
    3.55    fun merge (x, y) = AList.merge (op =) (K true) (x, y))
    3.56  
    3.57 -val set_default_raw_param = Data.map o AList.update (op =) o unnegate_raw_param
    3.58 +val set_default_raw_param =
    3.59 +  Data.map o fold (AList.update (op =)) o normalize_raw_param
    3.60  val default_raw_params = Data.get
    3.61  
    3.62  fun is_punctuation s = (s = "," orelse s = "-" orelse s = "\<midarrow>")
    3.63 @@ -145,7 +147,7 @@
    3.64  
    3.65  fun extract_params ctxt auto default_params override_params =
    3.66    let
    3.67 -    val override_params = map unnegate_raw_param override_params
    3.68 +    val override_params = maps normalize_raw_param override_params
    3.69      val raw_params = rev override_params @ rev default_params
    3.70      val lookup =
    3.71        Option.map stringify_raw_param_value o AList.lookup (op =) raw_params
    3.72 @@ -250,9 +252,8 @@
    3.73      val timeout = if auto then NONE else lookup_time "timeout"
    3.74      val tac_timeout = lookup_time "tac_timeout"
    3.75      val max_threads = Int.max (0, lookup_int "max_threads")
    3.76 -    val show_all = debug orelse lookup_bool "show_all"
    3.77 -    val show_datatypes = show_all orelse lookup_bool "show_datatypes"
    3.78 -    val show_consts = show_all orelse lookup_bool "show_consts"
    3.79 +    val show_datatypes = debug orelse lookup_bool "show_datatypes"
    3.80 +    val show_consts = debug orelse lookup_bool "show_consts"
    3.81      val formats = lookup_ints_assigns read_term_polymorphic "format" 0
    3.82      val evals = lookup_term_list "eval"
    3.83      val max_potential =