prompt: plain string, not output;
authorwenzelm
Mon Jul 09 11:44:22 2007 +0200 (2007-07-09)
changeset 23661b3f05bc680b6
parent 23660 18765718cf62
child 23662 91d06b04951f
prompt: plain string, not output;
src/Pure/General/source.ML
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/General/source.ML	Mon Jul 09 11:44:20 2007 +0200
     1.2 +++ b/src/Pure/General/source.ML	Mon Jul 09 11:44:22 2007 +0200
     1.3 @@ -122,7 +122,7 @@
     1.4    let val input = slurp_input instream in
     1.5      if exists (fn c => c = "\n") input then (input, ())
     1.6      else
     1.7 -      (TextIO.output (outstream, prompt);
     1.8 +      (TextIO.output (outstream, Output.output prompt);
     1.9          TextIO.flushOut outstream;
    1.10          (case TextIO.inputLine instream of
    1.11            SOME line => (input @ explode line, ())
     2.1 --- a/src/Pure/Isar/toplevel.ML	Mon Jul 09 11:44:20 2007 +0200
     2.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Jul 09 11:44:22 2007 +0200
     2.3 @@ -753,7 +753,9 @@
     2.4    in if secure then warning "Cannot exit to ML in secure mode" else (); secure end;
     2.5  
     2.6  fun raw_loop src =
     2.7 -  let val prompt = Source.default_prompt |> (Pretty.mode_markup Markup.prompt |-> enclose) in
     2.8 +  let val prompt =
     2.9 +    Output.escape (Source.default_prompt |> (Pretty.mode_markup Markup.prompt |-> enclose))
    2.10 +  in
    2.11      (case get_interrupt (Source.set_prompt prompt src) of
    2.12        NONE => (writeln "\nInterrupt."; raw_loop src)
    2.13      | SOME NONE => if warn_secure () then quit () else ()