# HG changeset patch
# User wenzelm
# Date 1197663336 -3600
# Node ID 98dd706319a1b1b695a87e55d54bc71b3e7d8027
# Parent  f7c6ca73a8bd9244c46a353ea6b85d0e318aa4de
tuned;

diff -r f7c6ca73a8bd -r 98dd706319a1 src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Dec 14 21:15:35 2007 +0100
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Dec 14 21:15:36 2007 +0100
@@ -100,15 +100,18 @@
 (* common markup *)
 
 fun proof_general_markup (name, props) =
-  (if name = Markup.promptN then ("", special "372")
-    else if name = Markup.stateN then (special "366" ^ "\n", "\n" ^ special "367")
-    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 IsabelleProcess.test_markupN) ?
-      (fn (bg1, en1) =>
-        let val (bg2, en2) = IsabelleProcess.test_markup (name, props)
-        in (bg1 ^ bg2, en2 ^ en1) end);
+  let
+    val (bg1, en1) =
+      if name = Markup.promptN then ("", special "372")
+      else if name = Markup.stateN then (special "366" ^ "\n", "\n" ^ special "367")
+      else if name = Markup.sendbackN then (special "376", special "377")
+      else if name = Markup.hiliteN then (special "327", special "330")
+      else ("", "");
+    val (bg2, en2) =
+      if name <> Markup.promptN andalso print_mode_active IsabelleProcess.test_markupN
+      then IsabelleProcess.test_markup (name, props)
+      else ("", "");
+  in (bg1 ^ bg2, en2 ^ en1) end;
 
 val _ = Markup.add_mode proof_generalN proof_general_markup;