diff options
Diffstat (limited to 'toplevel/toplevel.ml')
| -rw-r--r-- | toplevel/toplevel.ml | 23 |
1 files changed, 12 insertions, 11 deletions
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 439e9254..39106bbf 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: toplevel.ml 9252 2006-10-20 14:22:41Z herbelin $ *) +(* $Id: toplevel.ml 9432 2006-12-12 09:07:36Z courtieu $ *) open Pp open Util @@ -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 "<prompt>" else "" +let emacs_prompt_startstring() = Printer.emacs_str "" "<prompt>" -let emacs_prompt_endstring() = - if !Options.print_emacs_safechar then "</prompt>" - else String.make 1 (Char.chr 249) +let emacs_prompt_endstring() = Printer.emacs_str (String.make 1 (Char.chr 249)) "</prompt>" (* Read a char in an input channel, displaying a prompt at every beginning of line. *) @@ -223,16 +220,20 @@ let make_emacs_prompt() = (fun acc x -> acc ^ (if acc <> "" then "|" else "") ^ Names.string_of_id x) "" pending in let proof_info = if dpth >= 0 then string_of_int dpth else "0" in - statnum ^ " |" ^ pendingprompt ^ "| " ^ proof_info ^ " < " ^ (emacs_prompt_endstring()) +(* statnum ^ " |" ^ pendingprompt ^ "| " ^ proof_info ^ " < " ^ (emacs_prompt_endstring()) *) + if !Options.print_emacs then statnum ^ " |" ^ pendingprompt ^ "| " ^ proof_info ^ " < " + else "" + (* A buffer to store the current command read on stdin. It is * initialized when a vernac command is immediately followed by "\n", * 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() + ^ emacs_prompt_endstring() in { prompt = pr; str = ""; @@ -244,9 +245,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. *) |