src/Pure/Isar/toplevel.ML
changeset 23661 b3f05bc680b6
parent 23646 df8103fc3c8a
child 23701 1716f19e7d25
--- 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 ()