turn constraints into Isabelle_Markup.typing, depending on show_markup options;
proper recursion in standard_format;

--- a/src/Pure/General/pretty.scala	Sat Sep 29 16:15:18 2012 +0200
+++ b/src/Pure/General/pretty.scala	Sat Sep 29 16:17:46 2012 +0200
@@ -67,7 +67,7 @@
   def standard_format(body: XML.Body): XML.Body =
     body flatMap {
       case XML.Wrapped_Elem(markup, body1, body2) =>
-        List(XML.Wrapped_Elem(markup, body1, standard_format(body)))
+        List(XML.Wrapped_Elem(markup, body1, standard_format(body2)))
       case XML.Elem(markup, body) => List(XML.Elem(markup, standard_format(body)))
       case XML.Text(text) => Library.separate(FBreak, split_lines(text).map(XML.Text))
     }

--- a/src/Pure/Isar/attrib.ML	Sat Sep 29 16:15:18 2012 +0200
+++ b/src/Pure/Isar/attrib.ML	Sat Sep 29 16:17:46 2012 +0200
@@ -519,6 +519,7 @@
   register_config Printer.show_brackets_raw #>
   register_config Printer.show_sorts_raw #>
   register_config Printer.show_types_raw #>
+  register_config Printer.show_markup_raw #>
   register_config Printer.show_structs_raw #>
   register_config Printer.show_question_marks_raw #>
   register_config Syntax.ambiguity_warning_raw #>

--- a/src/Pure/Syntax/printer.ML	Sat Sep 29 16:15:18 2012 +0200
+++ b/src/Pure/Syntax/printer.ML	Sat Sep 29 16:17:46 2012 +0200
@@ -11,6 +11,7 @@
   val show_sorts: bool Config.T
   val show_free_types: bool Config.T
   val show_all_types: bool Config.T
+  val show_markup: bool Config.T
   val show_structs: bool Config.T
   val show_question_marks: bool Config.T
   val pretty_priority: int Config.T
@@ -25,6 +26,8 @@
   val show_types_raw: Config.raw
   val show_sorts_default: bool Unsynchronized.ref
   val show_sorts_raw: Config.raw
+  val show_markup_default: bool Unsynchronized.ref
+  val show_markup_raw: Config.raw
   val show_structs_raw: Config.raw
   val show_question_marks_default: bool Unsynchronized.ref
   val show_question_marks_raw: Config.raw
@@ -65,6 +68,10 @@
 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_markup_default = Unsynchronized.ref false;
+val show_markup_raw = Config.declare "show_markup" (fn _ => Config.Bool (! show_markup_default));
+val show_markup = Config.bool show_markup_raw;
+
 val show_structs_raw = Config.declare "show_structs" (fn _ => Config.Bool false);
 val show_structs = Config.bool show_structs_raw;
 

--- a/src/Pure/Syntax/syntax_phases.ML	Sat Sep 29 16:15:18 2012 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Sat Sep 29 16:17:46 2012 +0200
@@ -499,6 +499,7 @@
     val show_structs = Config.get ctxt show_structs;
     val show_free_types = Config.get ctxt show_free_types;
     val show_all_types = Config.get ctxt show_all_types;
+    val show_markup = Config.get ctxt show_markup;
 
     val {structs, fixes} = idents;
 
@@ -563,14 +564,14 @@
       handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)
 
     and constrain t T =
-      if show_types andalso T <> dummyT then
+      if (show_types orelse show_markup) andalso T <> dummyT then
         Ast.Appl [Ast.Constant "_constrain", simple_ast_of ctxt t,
           ast_of_termT ctxt trf (term_of_typ ctxt T)]
       else simple_ast_of ctxt t;
   in
     tm
     |> Syntax_Trans.prop_tr'
-    |> show_types ? (#1 o prune_typs o rpair [])
+    |> (show_types andalso not show_markup) ? (#1 o prune_typs o rpair [])
     |> mark_atoms
     |> ast_of
   end;
@@ -601,9 +602,26 @@
       | SOME x' => (Isabelle_Markup.skolem, Term.string_of_vname (x', i)))
   | NONE => (Isabelle_Markup.var, s));
 
+val typing_elem = YXML.output_markup_elem Isabelle_Markup.typing;
+
 fun unparse_t t_to_ast prt_t markup ctxt t =
   let
+    val show_markup = Config.get ctxt show_markup;
+
     val syn = Proof_Context.syn_of ctxt;
+    val prtabs = Syntax.prtabs syn;
+    val trf = Syntax.print_ast_translation syn;
+
+    fun markup_extern c =
+      (case Syntax.lookup_const syn c of
+        SOME "" => ([], c)
+      | SOME b => markup_extern b
+      | NONE => c |> Lexicon.unmark
+         {case_class = fn x => (markup_class ctxt x, Proof_Context.extern_class ctxt x),
+          case_type = fn x => (markup_type ctxt x, Proof_Context.extern_type ctxt x),
+          case_const = fn x => (markup_const ctxt x, Proof_Context.extern_const ctxt x),
+          case_fixed = fn x => free_or_skolem ctxt x,
+          case_default = fn x => ([], x)});
 
     fun token_trans "_tfree" x = SOME (Pretty.mark_str (Isabelle_Markup.tfree, x))
       | token_trans "_tvar" x = SOME (Pretty.mark_str (Isabelle_Markup.tvar, x))
@@ -616,23 +634,26 @@
       | token_trans _ _ = NONE;
 
     fun markup_trans a [Ast.Variable x] = token_trans a x
-      | markup_trans _ _ = NONE;
+      | markup_trans "_constrain" [t, ty] =
+          if show_markup then
+            let
+              val ((bg1, bg2), en) = typing_elem;
+              val bg = bg1 ^ Pretty.symbolic_output (pretty_typ_ast Markup.empty ty) ^ bg2;
+            in SOME (Pretty.raw_markup (bg, en) (0, [pretty_ast Markup.empty t])) end
+          else NONE
+      | markup_trans _ _ = NONE
 
-    fun markup_extern c =
-      (case Syntax.lookup_const syn c of
-        SOME "" => ([], c)
-      | SOME b => markup_extern b
-      | NONE => c |> Lexicon.unmark
-         {case_class = fn x => (markup_class ctxt x, Proof_Context.extern_class ctxt x),
-          case_type = fn x => (markup_type ctxt x, Proof_Context.extern_type ctxt x),
-          case_const = fn x => (markup_const ctxt x, Proof_Context.extern_const ctxt x),
-          case_fixed = fn x => free_or_skolem ctxt x,
-          case_default = fn x => ([], x)});
+    and pretty_typ_ast m ast = ast
+      |> Printer.pretty_typ_ast ctxt prtabs trf markup_trans markup_extern
+      |> Pretty.markup m
+
+    and pretty_ast m ast = ast
+      |> prt_t ctxt prtabs trf markup_trans markup_extern
+      |> Pretty.markup m;
   in
     t_to_ast ctxt (Syntax.print_translation syn) t
     |> Ast.normalize ctxt (Syntax.print_rules syn)
-    |> prt_t ctxt (Syntax.prtabs syn) (Syntax.print_ast_translation syn) markup_trans markup_extern
-    |> Pretty.markup markup
+    |> pretty_ast markup
   end;
 
 in