get rid of "show_all_types" in Nitpick
authorblanchet
Mon May 27 15:14:41 2013 +0200 (2013-05-27)
changeset 521747fd0b5cfbb79
parent 52173 ec337c3438a7
child 52180 55efdc47ebd1
get rid of "show_all_types" in Nitpick
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/Nitpick/nitpick_scope.ML
src/HOL/Tools/Nitpick/nitpick_util.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon May 27 15:13:34 2013 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon May 27 15:14:41 2013 +0200
     1.3 @@ -943,8 +943,8 @@
     1.4                                     T T' (rep_of name)
     1.5        in
     1.6          Pretty.block (Pretty.breaks
     1.7 -            [Syntax.pretty_term (set_show_all_types ctxt) t1,
     1.8 -             Pretty.str oper, Syntax.pretty_term ctxt t2])
     1.9 +            [Syntax.pretty_term ctxt t1, Pretty.str oper,
    1.10 +             Syntax.pretty_term ctxt t2])
    1.11        end
    1.12      fun pretty_for_datatype ({typ, card, complete, ...} : datatype_spec) =
    1.13        Pretty.block (Pretty.breaks
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Mon May 27 15:13:34 2013 +0200
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Mon May 27 15:14:41 2013 +0200
     2.3 @@ -142,10 +142,9 @@
     2.4     handle TYPE ("Nitpick_HOL.card_of_type", _, _) => ~1, offset_of_type ofs T)
     2.5  
     2.6  fun quintuple_for_scope code_type code_term code_string
     2.7 -        ({hol_ctxt = {ctxt = ctxt0, stds, ...}, card_assigns, bits, bisim_depth,
     2.8 +        ({hol_ctxt = {ctxt, stds, ...}, card_assigns, bits, bisim_depth,
     2.9           datatypes, ...} : scope) =
    2.10    let
    2.11 -    val ctxt = set_show_all_types ctxt0
    2.12      val boring_Ts = [@{typ unsigned_bit}, @{typ signed_bit},
    2.13                       @{typ bisim_iterator}]
    2.14      val (iter_assigns, card_assigns) =
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Mon May 27 15:13:34 2013 +0200
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Mon May 27 15:14:41 2013 +0200
     3.3 @@ -72,7 +72,6 @@
     3.4    val eta_expand : typ list -> term -> int -> term
     3.5    val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b
     3.6    val DETERM_TIMEOUT : Time.time option -> tactic -> tactic
     3.7 -  val set_show_all_types : Proof.context -> Proof.context
     3.8    val indent_size : int
     3.9    val pstrs : string -> Pretty.T list
    3.10    val unyxml : string -> string
    3.11 @@ -288,11 +287,6 @@
    3.12  fun DETERM_TIMEOUT delay tac st =
    3.13    Seq.of_list (the_list (time_limit delay (fn () => SINGLE tac st) ()))
    3.14  
    3.15 -fun set_show_all_types ctxt =
    3.16 -  Config.put show_all_types
    3.17 -    (Config.get ctxt show_types orelse Config.get ctxt show_sorts
    3.18 -      orelse Config.get ctxt show_all_types) ctxt
    3.19 -
    3.20  val indent_size = 2
    3.21  
    3.22  val pstrs = Pretty.breaks o map Pretty.str o space_explode " "