--- a/src/Pure/Syntax/printer.ML Fri Sep 03 14:20:47 2010 +0200
+++ b/src/Pure/Syntax/printer.ML Fri Sep 03 15:54:03 2010 +0200
@@ -9,7 +9,9 @@
val show_brackets: bool Unsynchronized.ref
val show_sorts: bool Unsynchronized.ref
val show_types: bool Unsynchronized.ref
- val show_no_free_types: bool Unsynchronized.ref
+ val show_free_types_default: bool Unsynchronized.ref
+ val show_free_types_value: Config.value Config.T
+ val show_free_types: bool Config.T
val show_all_types: bool Unsynchronized.ref
val show_structs: bool Unsynchronized.ref
val show_question_marks_default: bool Unsynchronized.ref
@@ -51,10 +53,14 @@
val show_types = Unsynchronized.ref false;
val show_sorts = Unsynchronized.ref false;
val show_brackets = Unsynchronized.ref false;
-val show_no_free_types = Unsynchronized.ref false;
val show_all_types = Unsynchronized.ref false;
val show_structs = Unsynchronized.ref false;
+val show_free_types_default = Unsynchronized.ref true;
+val show_free_types_value =
+ Config.declare false "show_free_types" (fn _ => Config.Bool (! show_free_types_default));
+val show_free_types = Config.bool show_free_types_value;
+
val show_question_marks_default = Unsynchronized.ref true;
val show_question_marks_value =
Config.declare false "show_question_marks" (fn _ => Config.Bool (! show_question_marks_default));
@@ -120,8 +126,9 @@
(** term_to_ast **)
fun ast_of_term idents consts ctxt trf
- show_all_types no_freeTs show_types show_sorts show_structs tm =
+ show_all_types show_types show_sorts show_structs tm =
let
+ val show_free_types = Config.get ctxt show_free_types;
val {structs, fixes} = idents;
fun mark_atoms ((t as Const (c, T)) $ u) =
@@ -148,11 +155,11 @@
fun prune_typs (t_seen as (Const _, _)) = t_seen
| prune_typs (t as Free (x, ty), seen) =
if ty = dummyT then (t, seen)
- else if no_freeTs orelse member (op aconv) seen t then (Lexicon.free x, seen)
+ else if not show_free_types orelse member (op aconv) seen t then (Lexicon.free x, seen)
else (t, t :: seen)
| prune_typs (t as Var (xi, ty), seen) =
if ty = dummyT then (t, seen)
- else if no_freeTs orelse member (op aconv) seen t then (Lexicon.var xi, seen)
+ else if not show_free_types orelse member (op aconv) seen t then (Lexicon.var xi, seen)
else (t, t :: seen)
| prune_typs (t_seen as (Bound _, _)) = t_seen
| prune_typs (Abs (x, ty, t), seen) =
@@ -199,7 +206,7 @@
end;
fun term_to_ast idents consts ctxt trf tm =
- ast_of_term idents consts ctxt trf (! show_all_types) (! show_no_free_types)
+ ast_of_term idents consts ctxt trf (! show_all_types)
(! show_types orelse ! show_sorts orelse ! show_all_types) (! show_sorts) (! show_structs) tm;