summaryrefslogtreecommitdiff
path: root/toplevel/toplevel.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
commite978da8c41d8a3c19a29036d9c569fbe2a4616b0 (patch)
tree0de2a907ee93c795978f3c843155bee91c11ed60 /toplevel/toplevel.ml
parent3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff)
Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta
Diffstat (limited to 'toplevel/toplevel.ml')
-rw-r--r--toplevel/toplevel.ml8
1 files changed, 5 insertions, 3 deletions
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index a5c2564c..95c1b7d9 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: toplevel.ml 6947 2005-04-20 16:18:41Z coq $ *)
+(* $Id: toplevel.ml 8748 2006-04-27 16:01:26Z courtieu $ *)
open Pp
open Util
@@ -47,9 +47,12 @@ let resynch_buffer ibuf =
ibuf.start <- ibuf.start + ll
| _ -> ()
+
(* Read a char in an input channel, displaying a prompt at every
beginning of line. *)
+let emacs_prompt_endstring = String.make 1 (Char.chr 249)
+
let prompt_char ic ibuf count =
let bol = match ibuf.bols with
| ll::_ -> ibuf.len == ll
@@ -204,7 +207,6 @@ let make_prompt () =
*)
let make_emacs_prompt() =
let statnum = string_of_int (Lib.current_command_label ()) in
- let endchar = String.make 1 (Char.chr 249) in
let dpth = Pfedit.current_proof_depth() in
let pending = Pfedit.get_all_proof_names() in
let pendingprompt =
@@ -212,7 +214,7 @@ 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 ^ " < " ^ endchar
+ statnum ^ " |" ^ pendingprompt ^ "| " ^ proof_info ^ " < " ^ emacs_prompt_endstring
(* A buffer to store the current command read on stdin. It is
* initialized when a vernac command is immediately followed by "\n",