--- a/src/Pure/Syntax/printer.ML Fri Sep 03 16:36:33 2010 +0200
+++ b/src/Pure/Syntax/printer.ML Fri Sep 03 17:43:44 2010 +0200
@@ -10,7 +10,7 @@
val show_sorts: bool Unsynchronized.ref
val show_types: bool Unsynchronized.ref
val show_free_types: bool Config.T
- val show_all_types: bool Unsynchronized.ref
+ val show_all_types: bool Config.T
val show_structs: bool Unsynchronized.ref
val show_question_marks_default: bool Unsynchronized.ref
val show_question_marks_value: Config.value Config.T
@@ -51,11 +51,10 @@
val show_types = Unsynchronized.ref false;
val show_sorts = Unsynchronized.ref false;
val show_brackets = Unsynchronized.ref false;
-val show_all_types = Unsynchronized.ref false;
+val show_free_types = Config.bool (Config.declare "show_free_types" (fn _ => Config.Bool true));
+val show_all_types = Config.bool (Config.declare "show_all_types" (fn _ => Config.Bool false));
val show_structs = Unsynchronized.ref false;
-val show_free_types = Config.bool (Config.declare "show_free_types" (fn _ => Config.Bool true));
-
val show_question_marks_default = Unsynchronized.ref true;
val show_question_marks_value =
Config.declare "show_question_marks" (fn _ => Config.Bool (! show_question_marks_default));
@@ -120,10 +119,11 @@
(** term_to_ast **)
-fun ast_of_term idents consts ctxt trf
- show_all_types show_types show_sorts show_structs tm =
+fun ast_of_term idents consts ctxt trf show_types show_sorts show_structs tm =
let
val show_free_types = Config.get ctxt show_free_types;
+ val show_all_types = Config.get ctxt show_all_types;
+
val {structs, fixes} = idents;
fun mark_atoms ((t as Const (c, T)) $ u) =
@@ -201,8 +201,9 @@
end;
fun term_to_ast idents consts ctxt trf tm =
- ast_of_term idents consts ctxt trf (! show_all_types)
- (! show_types orelse ! show_sorts orelse ! show_all_types) (! show_sorts) (! show_structs) tm;
+ ast_of_term idents consts ctxt trf
+ (! show_types orelse ! show_sorts orelse Config.get ctxt show_all_types)
+ (! show_sorts) (! show_structs) tm;