# HG changeset patch # User wenzelm # Date 1196896892 -3600 # Node ID 06ffd67a5e79fa57088dcc16e2bc61c986b433d8 # Parent e4d465bc5b35d99f042c313eb0f3d87bc5c4169f moved basic test_markup to isabelle_process.ML; diff -r e4d465bc5b35 -r 06ffd67a5e79 src/Pure/ProofGeneral/proof_general_emacs.ML --- a/src/Pure/ProofGeneral/proof_general_emacs.ML Thu Dec 06 00:21:32 2007 +0100 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Thu Dec 06 00:21:32 2007 +0100 @@ -105,10 +105,10 @@ else if name = Markup.sendbackN then (special "376", special "377") else if name = Markup.hiliteN then (special "327", special "330") else ("", "")) - |> (name <> Markup.promptN andalso print_mode_active "test_markup") ? - (fn (bg, en) => - (bg ^ enclose "<" ">" (space_implode " " (name :: map XML.attribute props)), - enclose "" name ^ en)); + |> (name <> Markup.promptN andalso print_mode_active IsabelleProcess.test_markupN) ? + (fn (bg1, en1) => + let val (bg2, en2) = IsabelleProcess.test_markup (name, props) + in (bg1 ^ bg2, en2 ^ en1) end); val _ = Markup.add_mode proof_generalN proof_general_markup;