# HG changeset patch
# User wenzelm
# Date 1184102984 -7200
# Node ID d0d583c7a41f54bf2b79e1f3bc0fa9470463dbc6
# Parent  ccd9cb15c062c3dca679e34c06208ae70cdf4e2b
Markup.enclose;

diff -r ccd9cb15c062 -r d0d583c7a41f src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Tue Jul 10 23:29:43 2007 +0200
+++ b/src/Pure/General/position.ML	Tue Jul 10 23:29:44 2007 +0200
@@ -65,8 +65,7 @@
   | print (Pos (SOME n, SOME s)) = "(line " ^ string_of_int n ^ " of " ^ quote s ^ ")";
 
 fun str_of (Pos (NONE, NONE)) = ""
-  | str_of pos = " " ^
-      (Markup.output (Markup.properties (properties_of pos) Markup.position) |-> enclose)
-        (print pos);
+  | str_of pos =
+      " " ^ Markup.enclose (Markup.properties (properties_of pos) Markup.position) (print pos);
 
 end;
diff -r ccd9cb15c062 -r d0d583c7a41f src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Jul 10 23:29:43 2007 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Jul 10 23:29:44 2007 +0200
@@ -751,9 +751,7 @@
   in if secure then warning "Cannot exit to ML in secure mode" else (); secure end;
 
 fun raw_loop src =
-  let val prompt =
-    Output.escape ((Markup.output Markup.prompt |-> enclose) Source.default_prompt)
-  in
+  let val prompt = Output.escape (Markup.enclose Markup.prompt Source.default_prompt) in
     (case get_interrupt (Source.set_prompt prompt src) of
       NONE => (writeln "\nInterrupt."; raw_loop src)
     | SOME NONE => if warn_secure () then quit () else ()