1.1 --- a/src/Pure/Isar/toplevel.ML	Mon Jul 09 11:44:20 2007 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Jul 09 11:44:22 2007 +0200
     1.3 @@ -753,7 +753,9 @@
     1.4    in if secure then warning "Cannot exit to ML in secure mode" else (); secure end;
     1.5  
     1.6  fun raw_loop src =
     1.7 -  let val prompt = Source.default_prompt |> (Pretty.mode_markup Markup.prompt |-> enclose) in
     1.8 +  let val prompt =
     1.9 +    Output.escape (Source.default_prompt |> (Pretty.mode_markup Markup.prompt |-> enclose))
    1.10 +  in
    1.11      (case get_interrupt (Source.set_prompt prompt src) of
    1.12        NONE => (writeln "\nInterrupt."; raw_loop src)
    1.13      | SOME NONE => if warn_secure () then quit () else ()