src/Pure/Syntax/printer.ML
changeset 51949 f6858bb224c9
parent 49821 d15fe10593ff
child 52043 286629271d65
     1.1 --- a/src/Pure/Syntax/printer.ML	Sun May 12 19:56:30 2013 +0200
     1.2 +++ b/src/Pure/Syntax/printer.ML	Sun May 12 20:25:45 2013 +0200
     1.3 @@ -29,7 +29,6 @@
     1.4    val show_markup_default: bool Unsynchronized.ref
     1.5    val show_markup_raw: Config.raw
     1.6    val show_structs_raw: Config.raw
     1.7 -  val show_question_marks_default: bool Unsynchronized.ref
     1.8    val show_question_marks_raw: Config.raw
     1.9    val show_type_constraint: Proof.context -> bool
    1.10    val show_sort_constraint: Proof.context -> bool
    1.11 @@ -77,9 +76,7 @@
    1.12  val show_structs_raw = Config.declare "show_structs" (fn _ => Config.Bool false);
    1.13  val show_structs = Config.bool show_structs_raw;
    1.14  
    1.15 -val show_question_marks_default = Unsynchronized.ref true;
    1.16 -val show_question_marks_raw =
    1.17 -  Config.declare "show_question_marks" (fn _ => Config.Bool (! show_question_marks_default));
    1.18 +val show_question_marks_raw = Config.declare_option "show_question_marks";
    1.19  val show_question_marks = Config.bool show_question_marks_raw;
    1.20  
    1.21  fun show_type_constraint ctxt = Config.get ctxt show_types orelse Config.get ctxt show_markup;