moved basic test_markup to isabelle_process.ML;
authorwenzelm
Thu, 06 Dec 2007 00:21:32 +0100
changeset 25553 06ffd67a5e79
parent 25552 e4d465bc5b35
child 25554 082d97057e23
moved basic test_markup to isabelle_process.ML;
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;