diff options
Diffstat (limited to 'toplevel/toplevel.ml')
| -rw-r--r-- | toplevel/toplevel.ml | 28 |
1 files changed, 21 insertions, 7 deletions
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 95c1b7d9..439e9254 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: toplevel.ml 8748 2006-04-27 16:01:26Z courtieu $ *) +(* $Id: toplevel.ml 9252 2006-10-20 14:22:41Z herbelin $ *) open Pp open Util @@ -48,11 +48,19 @@ let resynch_buffer ibuf = | _ -> () -(* Read a char in an input channel, displaying a prompt at every - beginning of line. *) +(* emacs special character for prompt end (fast) detection. Prefer + (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_endstring = String.make 1 (Char.chr 249) +let emacs_prompt_endstring() = + if !Options.print_emacs_safechar then "</prompt>" + else String.make 1 (Char.chr 249) +(* Read a char in an input channel, displaying a prompt at every + beginning of line. *) let prompt_char ic ibuf count = let bol = match ibuf.bols with | ll::_ -> ibuf.len == ll @@ -128,6 +136,7 @@ let print_highlight_location ib loc = str sn ++ str dn) in (l1 ++ li ++ ln) in + let loc = make_loc (bp,ep) in (str"Toplevel input, characters " ++ Cerrors.print_loc loc ++ fnl () ++ highlight_lines ++ fnl ()) @@ -214,14 +223,16 @@ 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()) (* 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() = - make_prompt() ^ Printer.emacs_str (make_emacs_prompt()) + Printer.emacs_str (emacs_prompt_startstring()) + ^ make_prompt() + ^ Printer.emacs_str (make_emacs_prompt()) in { prompt = pr; str = ""; @@ -232,7 +243,10 @@ let top_buffer = let set_prompt prompt = top_buffer.prompt - <- (fun () -> (prompt ())^(Printer.emacs_str (String.make 1 (Char.chr 249)))) + <- (fun () -> + Printer.emacs_str (emacs_prompt_startstring()) + ^ prompt () + ^ Printer.emacs_str (emacs_prompt_endstring())) (* Removes and prints the location of the error. The following exceptions need not be located. *) |