# HG changeset patch
# User wenzelm
# Date 1349276398 -7200
# Node ID a6814de45b69be668cdb7f00e11f89794f5f484d
# Parent  b8a710806de997d653730b84c7912298ad2b08e3
more explicit show_type_constraint, show_sort_constraint;

diff -r b8a710806de9 -r a6814de45b69 src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Wed Oct 03 16:59:20 2012 +0200
+++ b/src/HOL/Groups.thy	Wed Oct 03 16:59:58 2012 +0200
@@ -124,8 +124,8 @@
 typed_print_translation (advanced) {*
   let
     fun tr' c = (c, fn ctxt => fn T => fn ts =>
-      if not (null ts) orelse T = dummyT
-        orelse not (Config.get ctxt show_types) andalso can Term.dest_Type T
+      if not (null ts) orelse T = dummyT orelse
+        not (Printer.show_type_constraint ctxt) andalso can Term.dest_Type T
       then raise Match
       else
         Syntax.const @{syntax_const "_constrain"} $ Syntax.const c $
diff -r b8a710806de9 -r a6814de45b69 src/HOL/Num.thy
--- a/src/HOL/Num.thy	Wed Oct 03 16:59:20 2012 +0200
+++ b/src/HOL/Num.thy	Wed Oct 03 16:59:58 2012 +0200
@@ -323,7 +323,7 @@
     in
       case T of
         Type (@{type_name fun}, [_, T']) =>
-          if not (Config.get ctxt show_types) andalso can Term.dest_Type T' then t'
+          if not (Printer.show_type_constraint ctxt) andalso can Term.dest_Type T' then t'
           else Syntax.const @{syntax_const "_constrain"} $ t' $ Syntax_Phases.term_of_typ ctxt T'
       | T' => if T' = dummyT then t' else raise Match
     end;
diff -r b8a710806de9 -r a6814de45b69 src/HOL/ex/Numeral_Representation.thy
--- a/src/HOL/ex/Numeral_Representation.thy	Wed Oct 03 16:59:20 2012 +0200
+++ b/src/HOL/ex/Numeral_Representation.thy	Wed Oct 03 16:59:58 2012 +0200
@@ -308,7 +308,7 @@
     in
       case T of
         Type (@{type_name fun}, [_, T']) =>
-          if not (Config.get ctxt show_types) andalso can Term.dest_Type T' then t'
+          if not (Printer.show_type_constraint ctxt) andalso can Term.dest_Type T' then t'
           else Syntax.const @{syntax_const "_constrain"} $ t' $ Syntax_Phases.term_of_typ ctxt T'
       | T' => if T' = dummyT then t' else raise Match
     end;
diff -r b8a710806de9 -r a6814de45b69 src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Wed Oct 03 16:59:20 2012 +0200
+++ b/src/Pure/Syntax/printer.ML	Wed Oct 03 16:59:58 2012 +0200
@@ -31,6 +31,8 @@
   val show_structs_raw: Config.raw
   val show_question_marks_default: bool Unsynchronized.ref
   val show_question_marks_raw: Config.raw
+  val show_type_constraint: Proof.context -> bool
+  val show_sort_constraint: Proof.context -> bool
   type prtabs
   val empty_prtabs: prtabs
   val update_prtabs: string -> Syntax_Ext.xprod list -> prtabs -> prtabs
@@ -80,6 +82,9 @@
   Config.declare "show_question_marks" (fn _ => Config.Bool (! show_question_marks_default));
 val show_question_marks = Config.bool show_question_marks_raw;
 
+fun show_type_constraint ctxt = Config.get ctxt show_types orelse Config.get ctxt show_markup;
+fun show_sort_constraint ctxt = Config.get ctxt show_sorts orelse Config.get ctxt show_markup;
+
 
 
 (** type prtabs **)
diff -r b8a710806de9 -r a6814de45b69 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Wed Oct 03 16:59:20 2012 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Wed Oct 03 16:59:58 2012 +0200
@@ -450,11 +450,10 @@
 
 fun term_of_typ ctxt ty =
   let
-    val show_sorts = Config.get ctxt show_sorts;
-    val show_markup = Config.get ctxt show_markup;
+    val show_sort_constraint = Printer.show_sort_constraint ctxt;
 
     fun ofsort t raw_S =
-      if show_sorts orelse show_markup then
+      if show_sort_constraint then
         let val S = #2 (Term_Position.decode_positionS raw_S)
         in if S = dummyS then t else Syntax.const "_ofsort" $ t $ term_of_sort S end
       else t;