turned show_no_free_types into proper configuration option show_free_types, with flipped polarity;
authorwenzelm
Fri Sep 03 15:54:03 2010 +0200 (2010-09-03)
changeset 39115a00da1674c1c
parent 39114 240e2b41a041
child 39116 f14735a88886
turned show_no_free_types into proper configuration option show_free_types, with flipped polarity;
src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
src/Pure/Isar/attrib.ML
src/Pure/Syntax/printer.ML
src/Pure/goal_display.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Sep 03 14:20:47 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Sep 03 15:54:03 2010 +0200
     1.3 @@ -945,13 +945,13 @@
     1.4          step :: aux subst depth nextp proof
     1.5    in aux [] 0 (1, 1) end
     1.6  
     1.7 -fun string_for_proof ctxt full_types i n =
     1.8 +fun string_for_proof ctxt0 full_types i n =
     1.9    let
    1.10 +    val ctxt = Config.put show_free_types false ctxt0
    1.11      fun fix_print_mode f x =
    1.12 -      setmp_CRITICAL show_no_free_types true
    1.13 -          (setmp_CRITICAL show_types true
    1.14 -               (Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
    1.15 -                                         (print_mode_value ())) f)) x
    1.16 +      setmp_CRITICAL show_types true
    1.17 +           (Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
    1.18 +                                     (print_mode_value ())) f) x
    1.19      fun do_indent ind = replicate_string (ind * indent_size) " "
    1.20      fun do_free (s, T) =
    1.21        maybe_quote s ^ " :: " ^
     2.1 --- a/src/Pure/Isar/attrib.ML	Fri Sep 03 14:20:47 2010 +0200
     2.2 +++ b/src/Pure/Isar/attrib.ML	Fri Sep 03 15:54:03 2010 +0200
     2.3 @@ -392,7 +392,8 @@
     2.4  (* theory setup *)
     2.5  
     2.6  val _ = Context.>> (Context.map_theory
     2.7 - (register_config Syntax.show_question_marks_value #>
     2.8 + (register_config Syntax.show_free_types_value #>
     2.9 +  register_config Syntax.show_question_marks_value #>
    2.10    register_config Goal_Display.show_consts_value #>
    2.11    register_config Unify.trace_bound_value #>
    2.12    register_config Unify.search_bound_value #>
     3.1 --- a/src/Pure/Syntax/printer.ML	Fri Sep 03 14:20:47 2010 +0200
     3.2 +++ b/src/Pure/Syntax/printer.ML	Fri Sep 03 15:54:03 2010 +0200
     3.3 @@ -9,7 +9,9 @@
     3.4    val show_brackets: bool Unsynchronized.ref
     3.5    val show_sorts: bool Unsynchronized.ref
     3.6    val show_types: bool Unsynchronized.ref
     3.7 -  val show_no_free_types: bool Unsynchronized.ref
     3.8 +  val show_free_types_default: bool Unsynchronized.ref
     3.9 +  val show_free_types_value: Config.value Config.T
    3.10 +  val show_free_types: bool Config.T
    3.11    val show_all_types: bool Unsynchronized.ref
    3.12    val show_structs: bool Unsynchronized.ref
    3.13    val show_question_marks_default: bool Unsynchronized.ref
    3.14 @@ -51,10 +53,14 @@
    3.15  val show_types = Unsynchronized.ref false;
    3.16  val show_sorts = Unsynchronized.ref false;
    3.17  val show_brackets = Unsynchronized.ref false;
    3.18 -val show_no_free_types = Unsynchronized.ref false;
    3.19  val show_all_types = Unsynchronized.ref false;
    3.20  val show_structs = Unsynchronized.ref false;
    3.21  
    3.22 +val show_free_types_default = Unsynchronized.ref true;
    3.23 +val show_free_types_value =
    3.24 +  Config.declare false "show_free_types" (fn _ => Config.Bool (! show_free_types_default));
    3.25 +val show_free_types = Config.bool show_free_types_value;
    3.26 +
    3.27  val show_question_marks_default = Unsynchronized.ref true;
    3.28  val show_question_marks_value =
    3.29    Config.declare false "show_question_marks" (fn _ => Config.Bool (! show_question_marks_default));
    3.30 @@ -120,8 +126,9 @@
    3.31  (** term_to_ast **)
    3.32  
    3.33  fun ast_of_term idents consts ctxt trf
    3.34 -    show_all_types no_freeTs show_types show_sorts show_structs tm =
    3.35 +    show_all_types show_types show_sorts show_structs tm =
    3.36    let
    3.37 +    val show_free_types = Config.get ctxt show_free_types;
    3.38      val {structs, fixes} = idents;
    3.39  
    3.40      fun mark_atoms ((t as Const (c, T)) $ u) =
    3.41 @@ -148,11 +155,11 @@
    3.42      fun prune_typs (t_seen as (Const _, _)) = t_seen
    3.43        | prune_typs (t as Free (x, ty), seen) =
    3.44            if ty = dummyT then (t, seen)
    3.45 -          else if no_freeTs orelse member (op aconv) seen t then (Lexicon.free x, seen)
    3.46 +          else if not show_free_types orelse member (op aconv) seen t then (Lexicon.free x, seen)
    3.47            else (t, t :: seen)
    3.48        | prune_typs (t as Var (xi, ty), seen) =
    3.49            if ty = dummyT then (t, seen)
    3.50 -          else if no_freeTs orelse member (op aconv) seen t then (Lexicon.var xi, seen)
    3.51 +          else if not show_free_types orelse member (op aconv) seen t then (Lexicon.var xi, seen)
    3.52            else (t, t :: seen)
    3.53        | prune_typs (t_seen as (Bound _, _)) = t_seen
    3.54        | prune_typs (Abs (x, ty, t), seen) =
    3.55 @@ -199,7 +206,7 @@
    3.56    end;
    3.57  
    3.58  fun term_to_ast idents consts ctxt trf tm =
    3.59 -  ast_of_term idents consts ctxt trf (! show_all_types) (! show_no_free_types)
    3.60 +  ast_of_term idents consts ctxt trf (! show_all_types)
    3.61      (! show_types orelse ! show_sorts orelse ! show_all_types) (! show_sorts) (! show_structs) tm;
    3.62  
    3.63  
     4.1 --- a/src/Pure/goal_display.ML	Fri Sep 03 14:20:47 2010 +0200
     4.2 +++ b/src/Pure/goal_display.ML	Fri Sep 03 15:54:03 2010 +0200
     4.3 @@ -63,8 +63,10 @@
     4.4  
     4.5  in
     4.6  
     4.7 -fun pretty_goals ctxt {total, main, maxgoals} state =
     4.8 +fun pretty_goals ctxt0 {total, main, maxgoals} state =
     4.9    let
    4.10 +    val ctxt = Config.put show_free_types false ctxt0;
    4.11 +
    4.12      val prt_sort = Syntax.pretty_sort ctxt;
    4.13      val prt_typ = Syntax.pretty_typ ctxt;
    4.14      val prt_term = Syntax.pretty_term ctxt;
    4.15 @@ -115,9 +117,8 @@
    4.16        (if types then pretty_vars prop else []) @
    4.17        (if sorts then pretty_varsT prop else []);
    4.18    in
    4.19 -    setmp_CRITICAL show_no_free_types true
    4.20 -      (setmp_CRITICAL show_types (! show_types orelse ! show_sorts orelse ! show_all_types)
    4.21 -        (setmp_CRITICAL show_sorts false pretty_gs))
    4.22 +    setmp_CRITICAL show_types (! show_types orelse ! show_sorts orelse ! show_all_types)
    4.23 +      (setmp_CRITICAL show_sorts false pretty_gs)
    4.24     (! show_types orelse ! show_sorts orelse ! show_all_types, ! show_sorts)
    4.25    end;
    4.26