# HG changeset patch # User wenzelm # Date 1348928266 -7200 # Node ID 40e4feac2921c5eb14e0e07ecfef4b4b9515fe60 # Parent 7ff712de5747632877f3093a8246d476358be01f turn constraints into Isabelle_Markup.typing, depending on show_markup options; proper recursion in standard_format; diff -r 7ff712de5747 -r 40e4feac2921 src/Pure/General/pretty.scala --- 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)) } diff -r 7ff712de5747 -r 40e4feac2921 src/Pure/Isar/attrib.ML --- 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 #> diff -r 7ff712de5747 -r 40e4feac2921 src/Pure/Syntax/printer.ML --- 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; diff -r 7ff712de5747 -r 40e4feac2921 src/Pure/Syntax/syntax_phases.ML --- 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