diff options
| author |  Samuel Mimram <smimram@debian.org> | 2006-06-16 14:41:51 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2006-06-16 14:41:51 +0000 |
| commit | e978da8c41d8a3c19a29036d9c569fbe2a4616b0 (patch) | |
| tree | 0de2a907ee93c795978f3c843155bee91c11ed60 /toplevel/toplevel.ml | |
| parent | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff) | |
Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta
Diffstat (limited to 'toplevel/toplevel.ml')
| -rw-r--r-- | toplevel/toplevel.ml | 8 |
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", |