# HG changeset patch # User wenzelm # Date 1230933697 -3600 # Node ID da275b7809bd91b2f4578c9848532fb424665cdb # Parent a205acc943562aefe2145542aea560608a38d2f5 xsymbols: use plain Symbol.output; explicit rendering of message body: print mode is always YXML, markup is only observed for singleton text (avoids overlap of inner tokens with certain status messages), test XML markup is outermost (allows Proof General font-lock); Markup.no_output; diff -r a205acc94356 -r da275b7809bd src/Pure/ProofGeneral/proof_general_emacs.ML --- a/src/Pure/ProofGeneral/proof_general_emacs.ML Fri Jan 02 22:54:04 2009 +0100 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Fri Jan 02 23:01:37 2009 +0100 @@ -23,75 +23,74 @@ val thm_depsN = "thm_deps"; (*meta-information about theorem deps*) val test_markupN = "test_markup"; (*XML markup for everything*) -val _ = Markup.add_mode test_markupN (fn (name, props) => - if name = Markup.promptN then ("", "") else XML.output_markup (name, props)); - fun special ch = Symbol.SOH ^ ch; -(* text output: print modes for xsymbol *) +(* render markup *) local -fun xsym_output "\\" = "\\\\" - | xsym_output s = if Symbol.is_raw s then Symbol.decode_raw s else s; - -fun xsymbols_output s = - if print_mode_active Symbol.xsymbolsN andalso exists_string (fn c => c = "\\") s then - let val syms = Symbol.explode s - in (implode (map xsym_output syms), Symbol.length syms) end - else Output.default_output s; +fun render_trees ts = fold render_tree ts +and render_tree (XML.Text s) = Buffer.add s + | render_tree (XML.Elem (name, props, ts)) = + let + val (bg1, en1) = + if name <> Markup.promptN andalso print_mode_active test_markupN + then XML.output_markup (name, props) + else Markup.no_output; + val (bg2, en2) = + if (case ts of [XML.Text _] => false | _ => true) then Markup.no_output + else if name = Markup.stateN then (special "O" ^ "\n", "\n" ^ special "P") + else if name = Markup.sendbackN then (special "W", special "X") + else if name = Markup.hiliteN then (special "0", special "1") + else if name = Markup.tclassN then (special "B", special "A") + else if name = Markup.tfreeN then (special "C", special "A") + else if name = Markup.tvarN then (special "D", special "A") + else if name = Markup.freeN then (special "E", special "A") + else if name = Markup.boundN then (special "F", special "A") + else if name = Markup.varN then (special "G", special "A") + else if name = Markup.skolemN then (special "H", special "A") + else Markup.no_output; + in + Buffer.add bg1 #> + Buffer.add bg2 #> + render_trees ts #> + Buffer.add en2 #> + Buffer.add en1 + end; in -fun setup_xsymbols_output () = - Output.add_mode Symbol.xsymbolsN xsymbols_output Symbol.encode_raw; +fun render text = + Buffer.content (render_trees (YXML.parse_body text) Buffer.empty); end; -(* common markup *) +(* messages *) + +fun message bg en prfx text = + (case render text of + "" => () + | s => Output.writeln_default (enclose bg en (prefix_lines prfx s))); -val _ = Markup.add_mode proof_generalN (fn (name, props) => - let - val (bg1, en1) = - if name = Markup.stateN then (special "O" ^ "\n", "\n" ^ special "P") - else if name = Markup.sendbackN then (special "W", special "X") - else if name = Markup.hiliteN then (special "0", special "1") - else if name = Markup.tclassN then (special "B", special "A") - else if name = Markup.tfreeN then (special "C", special "A") - else if name = Markup.tvarN then (special "D", special "A") - else if name = Markup.freeN then (special "E", special "A") - else if name = Markup.boundN then (special "F", special "A") - else if name = Markup.varN then (special "G", special "A") - else if name = Markup.skolemN then (special "H", special "A") - else ("", ""); - val (bg2, en2) = - if name <> Markup.promptN andalso print_mode_active test_markupN - then XML.output_markup (name, props) - else ("", ""); - in (bg1 ^ bg2, en2 ^ en1) end); +fun setup_messages () = + (Output.writeln_fn := message "" "" ""; + Output.status_fn := (fn s => ! Output.priority_fn s); + Output.priority_fn := message (special "I") (special "J") ""; + Output.tracing_fn := message (special "I" ^ special "V") (special "J") ""; + Output.debug_fn := message (special "K") (special "L") "+++ "; + Output.warning_fn := message (special "K") (special "L") "### "; + Output.error_fn := message (special "M") (special "N") "*** "; + Output.prompt_fn := (fn s => Output.std_output (render s ^ special "S"))); + +fun panic s = + (message (special "M") (special "N") "!!! " ("## SYSTEM EXIT ##\n" ^ s); exit 1); -(* messages and notification *) - -fun decorate bg en prfx = - Output.writeln_default o enclose bg en o prefix_lines prfx; +(* notification *) -fun setup_messages () = - (Output.writeln_fn := Output.writeln_default; - Output.status_fn := (fn "" => () | s => ! Output.priority_fn s); - Output.priority_fn := (fn s => decorate (special "I") (special "J") "" s); - Output.tracing_fn := (fn s => decorate (special "I" ^ special "V") (special "J") "" s); - Output.debug_fn := (fn s => decorate (special "K") (special "L") "+++ " s); - Output.warning_fn := (fn s => decorate (special "K") (special "L") "### " s); - Output.error_fn := (fn s => decorate (special "M") (special "N") "*** " s); - Output.prompt_fn := (fn s => Output.std_output (s ^ special "S"))); - -fun panic s = - (decorate (special "M") (special "N") "!!! " ("## SYSTEM EXIT ##\n" ^ s); exit 1); - -fun emacs_notify s = decorate (special "I") (special "J") "" s; +val emacs_notify = message (special "I") (special "J") ""; fun tell_clear_goals () = emacs_notify "Proof General, please clear the goals buffer."; @@ -233,7 +232,9 @@ | init true = (! initialized orelse (Output.no_warnings init_outer_syntax (); - setup_xsymbols_output (); + Output.add_mode Symbol.xsymbolsN Symbol.output Output.default_escape; + Output.add_mode proof_generalN Output.default_output Output.default_escape; + Markup.add_mode proof_generalN YXML.output_markup; setup_messages (); ProofGeneralPgip.init_pgip_channel (! Output.priority_fn); setup_thy_loader ();