# HG changeset patch # User wenzelm # Date 1348942430 -7200 # Node ID de6be6922c19aa381feea366baf275e7eb614dec # Parent ac48def96b697e5cbdfb7b4ca217309bc3c2673b proper handling of constraints stemming from idtyp_ast_tr'; diff -r ac48def96b69 -r de6be6922c19 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Sat Sep 29 19:28:03 2012 +0200 +++ b/src/Pure/Syntax/syntax_phases.ML Sat Sep 29 20:13:50 2012 +0200 @@ -641,15 +641,18 @@ | token_trans _ _ = NONE; fun markup_trans a [Ast.Variable x] = token_trans a x - | markup_trans "_constrain" [t, ty] = - 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; - in SOME (Pretty.raw_markup (bg, en) (0, [pretty_ast Markup.empty t])) end - else NONE + | markup_trans "_constrain" [t, ty] = constrain_trans t ty + | markup_trans "_idtyp" [t, ty] = constrain_trans t ty | markup_trans _ _ = NONE + and constrain_trans t ty = + 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; + in SOME (Pretty.raw_markup (bg, en) (0, [pretty_ast Markup.empty t])) end + else NONE + and pretty_typ_ast m ast = ast |> Printer.pretty_typ_ast ctxt prtabs trf markup_trans markup_extern |> Pretty.markup m