From 55ce117e8083477593cf1ff2e51a3641c7973830 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Tue, 13 Feb 2007 13:48:12 +0000
Subject: Imported Upstream version 8.1+dfsg

---
 toplevel/toplevel.ml | 23 ++++++++++++-----------
 1 file changed, 12 insertions(+), 11 deletions(-)

(limited to 'toplevel/toplevel.ml')

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. *)
-- 
cgit v1.2.3