# HG changeset patch
# User wenzelm
# Date 1196896890 -3600
# Node ID 87d89b0f847a5dfd96fadfb688c4eac45324bbd4
# Parent  c482262dd960e9c5eeee208678697261ec1e7e41
replaced Markup.enclose by Markup.markup, which operates on plain strings instead of raw output;

diff -r c482262dd960 -r 87d89b0f847a src/HOL/Tools/watcher.ML
--- a/src/HOL/Tools/watcher.ML	Thu Dec 06 00:21:28 2007 +0100
+++ b/src/HOL/Tools/watcher.ML	Thu Dec 06 00:21:30 2007 +0100
@@ -364,7 +364,7 @@
       val outlines = 
 	case split_lines s of
 	    [] => ["Received bad string: " ^ s]
-	  | line::lines => ["  Try this command:", (*Markup.enclose Markup.sendback*) line, ""]
+	  | line::lines => ["  Try this command:", (*Markup.markup Markup.sendback*) line, ""]
 	                   @ lines
   in priority (cat_lines (sgline::sgtx::outlines)) end;
   
diff -r c482262dd960 -r 87d89b0f847a src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Thu Dec 06 00:21:28 2007 +0100
+++ b/src/Pure/General/position.ML	Thu Dec 06 00:21:30 2007 +0100
@@ -66,6 +66,6 @@
 
 fun str_of (Pos (NONE, NONE)) = ""
   | str_of pos =
-      " " ^ Markup.enclose (Markup.properties (properties_of pos) Markup.position) (print pos);
+      " " ^ Markup.markup (Markup.properties (properties_of pos) Markup.position) (print pos);
 
 end;
diff -r c482262dd960 -r 87d89b0f847a src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Thu Dec 06 00:21:28 2007 +0100
+++ b/src/Pure/Isar/toplevel.ML	Thu Dec 06 00:21:30 2007 +0100
@@ -762,7 +762,7 @@
   let
     fun check_secure () =
       (if secure then warning "Secure loop -- cannot exit to ML" else (); secure);
-    val prompt = Output.escape (Markup.enclose Markup.prompt Source.default_prompt);
+    val prompt = Markup.markup Markup.prompt Source.default_prompt;
   in
     (case get_interrupt (Source.set_prompt prompt src) of
       NONE => (writeln "\nInterrupt."; raw_loop secure src)