# HG changeset patch
# User wenzelm
# Date 1348930264 -7200
# Node ID 251342b60a820950a0e56467f26b44325c29f82f
# Parent  ae8c8b745f825eaf6ca711c37bafd32d9f9d3cf2
explicit show_types takes preferenced over show_markup;

diff -r ae8c8b745f82 -r 251342b60a82 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Sat Sep 29 16:35:31 2012 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Sat Sep 29 16:51:04 2012 +0200
@@ -571,7 +571,7 @@
   in
     tm
     |> Syntax_Trans.prop_tr'
-    |> (show_types andalso not show_markup) ? (#1 o prune_typs o rpair [])
+    |> show_types ? (#1 o prune_typs o rpair [])
     |> mark_atoms
     |> ast_of
   end;
@@ -606,6 +606,9 @@
 
 fun unparse_t t_to_ast prt_t markup ctxt t =
   let
+    val show_types =
+      Config.get ctxt show_types orelse Config.get ctxt show_sorts orelse
+      Config.get ctxt show_all_types;
     val show_markup = Config.get ctxt show_markup;
 
     val syn = Proof_Context.syn_of ctxt;
@@ -635,7 +638,7 @@
 
     fun markup_trans a [Ast.Variable x] = token_trans a x
       | markup_trans "_constrain" [t, ty] =
-          if show_markup then
+          if not show_types andalso show_markup then
             let
               val ((bg1, bg2), en) = typing_elem;
               val bg = bg1 ^ Pretty.symbolic_output (pretty_typ_ast Markup.empty ty) ^ bg2;