src/Pure/Syntax/printer.ML
changeset 39115 a00da1674c1c
parent 38980 af73cf0dc31f
child 39116 f14735a88886
     1.1 --- a/src/Pure/Syntax/printer.ML	Fri Sep 03 14:20:47 2010 +0200
     1.2 +++ b/src/Pure/Syntax/printer.ML	Fri Sep 03 15:54:03 2010 +0200
     1.3 @@ -9,7 +9,9 @@
     1.4    val show_brackets: bool Unsynchronized.ref
     1.5    val show_sorts: bool Unsynchronized.ref
     1.6    val show_types: bool Unsynchronized.ref
     1.7 -  val show_no_free_types: bool Unsynchronized.ref
     1.8 +  val show_free_types_default: bool Unsynchronized.ref
     1.9 +  val show_free_types_value: Config.value Config.T
    1.10 +  val show_free_types: bool Config.T
    1.11    val show_all_types: bool Unsynchronized.ref
    1.12    val show_structs: bool Unsynchronized.ref
    1.13    val show_question_marks_default: bool Unsynchronized.ref
    1.14 @@ -51,10 +53,14 @@
    1.15  val show_types = Unsynchronized.ref false;
    1.16  val show_sorts = Unsynchronized.ref false;
    1.17  val show_brackets = Unsynchronized.ref false;
    1.18 -val show_no_free_types = Unsynchronized.ref false;
    1.19  val show_all_types = Unsynchronized.ref false;
    1.20  val show_structs = Unsynchronized.ref false;
    1.21  
    1.22 +val show_free_types_default = Unsynchronized.ref true;
    1.23 +val show_free_types_value =
    1.24 +  Config.declare false "show_free_types" (fn _ => Config.Bool (! show_free_types_default));
    1.25 +val show_free_types = Config.bool show_free_types_value;
    1.26 +
    1.27  val show_question_marks_default = Unsynchronized.ref true;
    1.28  val show_question_marks_value =
    1.29    Config.declare false "show_question_marks" (fn _ => Config.Bool (! show_question_marks_default));
    1.30 @@ -120,8 +126,9 @@
    1.31  (** term_to_ast **)
    1.32  
    1.33  fun ast_of_term idents consts ctxt trf
    1.34 -    show_all_types no_freeTs show_types show_sorts show_structs tm =
    1.35 +    show_all_types show_types show_sorts show_structs tm =
    1.36    let
    1.37 +    val show_free_types = Config.get ctxt show_free_types;
    1.38      val {structs, fixes} = idents;
    1.39  
    1.40      fun mark_atoms ((t as Const (c, T)) $ u) =
    1.41 @@ -148,11 +155,11 @@
    1.42      fun prune_typs (t_seen as (Const _, _)) = t_seen
    1.43        | prune_typs (t as Free (x, ty), seen) =
    1.44            if ty = dummyT then (t, seen)
    1.45 -          else if no_freeTs orelse member (op aconv) seen t then (Lexicon.free x, seen)
    1.46 +          else if not show_free_types orelse member (op aconv) seen t then (Lexicon.free x, seen)
    1.47            else (t, t :: seen)
    1.48        | prune_typs (t as Var (xi, ty), seen) =
    1.49            if ty = dummyT then (t, seen)
    1.50 -          else if no_freeTs orelse member (op aconv) seen t then (Lexicon.var xi, seen)
    1.51 +          else if not show_free_types orelse member (op aconv) seen t then (Lexicon.var xi, seen)
    1.52            else (t, t :: seen)
    1.53        | prune_typs (t_seen as (Bound _, _)) = t_seen
    1.54        | prune_typs (Abs (x, ty, t), seen) =
    1.55 @@ -199,7 +206,7 @@
    1.56    end;
    1.57  
    1.58  fun term_to_ast idents consts ctxt trf tm =
    1.59 -  ast_of_term idents consts ctxt trf (! show_all_types) (! show_no_free_types)
    1.60 +  ast_of_term idents consts ctxt trf (! show_all_types)
    1.61      (! show_types orelse ! show_sorts orelse ! show_all_types) (! show_sorts) (! show_structs) tm;
    1.62  
    1.63