# HG changeset patch
# User wenzelm
# Date 1183974262 -7200
# Node ID b3f05bc680b62e2e8ad0782b8686bfc40413319e
# Parent  18765718cf629f7961c2ad78711cb00596688074
prompt: plain string, not output;

diff -r 18765718cf62 -r b3f05bc680b6 src/Pure/General/source.ML
--- a/src/Pure/General/source.ML	Mon Jul 09 11:44:20 2007 +0200
+++ b/src/Pure/General/source.ML	Mon Jul 09 11:44:22 2007 +0200
@@ -122,7 +122,7 @@
   let val input = slurp_input instream in
     if exists (fn c => c = "\n") input then (input, ())
     else
-      (TextIO.output (outstream, prompt);
+      (TextIO.output (outstream, Output.output prompt);
         TextIO.flushOut outstream;
         (case TextIO.inputLine instream of
           SOME line => (input @ explode line, ())
diff -r 18765718cf62 -r b3f05bc680b6 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Mon Jul 09 11:44:20 2007 +0200
+++ b/src/Pure/Isar/toplevel.ML	Mon Jul 09 11:44:22 2007 +0200
@@ -753,7 +753,9 @@
   in if secure then warning "Cannot exit to ML in secure mode" else (); secure end;
 
 fun raw_loop src =
-  let val prompt = Source.default_prompt |> (Pretty.mode_markup Markup.prompt |-> enclose) in
+  let val prompt =
+    Output.escape (Source.default_prompt |> (Pretty.mode_markup Markup.prompt |-> enclose))
+  in
     (case get_interrupt (Source.set_prompt prompt src) of
       NONE => (writeln "\nInterrupt."; raw_loop src)
     | SOME NONE => if warn_secure () then quit () else ()