From 6f1a8d56bc5937c398c32256d5446447b6673940 Mon Sep 17 00:00:00 2001 From: courtieu Date: Fri, 17 Nov 2006 15:02:35 +0000 Subject: The emacs-U option now does not output *any* char above 250. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9384 85f007b7-540e-0410-9357-904b9bb8a0f7 --- toplevel/toplevel.ml | 15 ++++++--------- 1 file changed, 6 insertions(+), 9 deletions(-) (limited to 'toplevel/toplevel.ml') diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index ac8167f28..f75b8fc68 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -52,12 +52,9 @@ let resynch_buffer ibuf = (Char.chr 6) since it does not interfere with utf8. For compatibility we let (Char.chr 249) as default for a while. *) -let emacs_prompt_startstring() = - if !Options.print_emacs_safechar then "" else "" +let emacs_prompt_startstring() = Printer.emacs_str "" "" -let emacs_prompt_endstring() = - if !Options.print_emacs_safechar then "" - else String.make 1 (Char.chr 249) +let emacs_prompt_endstring() = Printer.emacs_str (String.make 1 (Char.chr 249)) "" (* Read a char in an input channel, displaying a prompt at every beginning of line. *) @@ -230,9 +227,9 @@ let make_emacs_prompt() = * or after a Drop. *) let top_buffer = let pr() = - Printer.emacs_str (emacs_prompt_startstring()) + emacs_prompt_startstring() ^ make_prompt() - ^ Printer.emacs_str (make_emacs_prompt()) + ^ make_emacs_prompt() in { prompt = pr; str = ""; @@ -244,9 +241,9 @@ let top_buffer = let set_prompt prompt = top_buffer.prompt <- (fun () -> - Printer.emacs_str (emacs_prompt_startstring()) + emacs_prompt_startstring() ^ prompt () - ^ Printer.emacs_str (emacs_prompt_endstring())) + ^ emacs_prompt_endstring()) (* Removes and prints the location of the error. The following exceptions need not be located. *) -- cgit v1.2.3