# HG changeset patch
# User wenzelm
# Date 1369751351 -7200
# Node ID 0226035df99d1b9bb846f99842504d439a522c55
# Parent  849cf98e03c36343e01dbae33d514729fce706d8
more explicit Printer.type_emphasis, depending on show_type_emphasis;
tuned signature;

diff -r 849cf98e03c3 -r 0226035df99d src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Tue May 28 13:14:31 2013 +0200
+++ b/src/HOL/Groups.thy	Tue May 28 16:29:11 2013 +0200
@@ -124,12 +124,10 @@
 typed_print_translation {*
   let
     fun tr' c = (c, fn ctxt => fn T => fn ts =>
-      if not (null ts) orelse T = dummyT orelse
-        not (Printer.show_type_constraint ctxt) andalso can Term.dest_Type T
-      then raise Match
-      else
+      if null ts andalso Printer.type_emphasis ctxt T then
         Syntax.const @{syntax_const "_constrain"} $ Syntax.const c $
-          Syntax_Phases.term_of_typ ctxt T);
+          Syntax_Phases.term_of_typ ctxt T
+      else raise Match);
   in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end;
 *} -- {* show types that are presumably too general *}
 
diff -r 849cf98e03c3 -r 0226035df99d src/HOL/Num.thy
--- a/src/HOL/Num.thy	Tue May 28 13:14:31 2013 +0200
+++ b/src/HOL/Num.thy	Tue May 28 16:29:11 2013 +0200
@@ -332,8 +332,10 @@
       in
         (case T of
           Type (@{type_name fun}, [_, 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'
+            if Printer.type_emphasis ctxt T' then
+              Syntax.const @{syntax_const "_constrain"} $ t' $
+                Syntax_Phases.term_of_typ ctxt T'
+            else t'
         | _ => if T = dummyT then t' else raise Match)
       end;
   in
diff -r 849cf98e03c3 -r 0226035df99d src/HOL/ex/Numeral_Representation.thy
--- a/src/HOL/ex/Numeral_Representation.thy	Tue May 28 13:14:31 2013 +0200
+++ b/src/HOL/ex/Numeral_Representation.thy	Tue May 28 16:29:11 2013 +0200
@@ -306,11 +306,13 @@
         val k = int_of_num' n;
         val t' = Syntax.const @{syntax_const "_Numerals"} $ Syntax.free ("#" ^ string_of_int k);
       in
-        case T of
+        (case T of
           Type (@{type_name fun}, [_, 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
+            if Printer.type_emphasis ctxt T' then
+              Syntax.const @{syntax_const "_constrain"} $ t' $
+                Syntax_Phases.term_of_typ ctxt T'
+            else t'
+        | T' => if T' = dummyT then t' else raise Match)
       end;
   in [(@{const_syntax of_num}, num_tr')] end
 *}
diff -r 849cf98e03c3 -r 0226035df99d src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Tue May 28 13:14:31 2013 +0200
+++ b/src/Pure/Syntax/printer.ML	Tue May 28 16:29:11 2013 +0200
@@ -26,8 +26,8 @@
   val show_markup_raw: Config.raw
   val show_structs_raw: Config.raw
   val show_question_marks_raw: Config.raw
-  val show_type_constraint: Proof.context -> bool
-  val show_sort_constraint: Proof.context -> bool
+  val show_type_emphasis: bool Config.T
+  val type_emphasis: Proof.context -> typ -> bool
   type prtabs
   val empty_prtabs: prtabs
   val update_prtabs: string -> Syntax_Ext.xprod list -> prtabs -> prtabs
@@ -70,8 +70,13 @@
 val show_question_marks_raw = Config.declare_option "show_question_marks";
 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;
+val show_type_emphasis =
+  Config.bool (Config.declare "show_type_emphasis" (fn _ => Config.Bool true));
+
+fun type_emphasis ctxt T =
+  T <> dummyT andalso
+    (Config.get ctxt show_types orelse Config.get ctxt show_markup orelse
+      Config.get ctxt show_type_emphasis andalso not (can dest_Type T));
 
 
 
diff -r 849cf98e03c3 -r 0226035df99d src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Tue May 28 13:14:31 2013 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Tue May 28 16:29:11 2013 +0200
@@ -470,10 +470,10 @@
 
 fun term_of_typ ctxt ty =
   let
-    val show_sort_constraint = Printer.show_sort_constraint ctxt;
+    val show_sorts = Config.get ctxt show_sorts orelse Config.get ctxt show_markup;
 
     fun ofsort t raw_S =
-      if show_sort_constraint then
+      if show_sorts 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;