diff options
| -rw-r--r-- | lib/options.ml | 1 | ||||
| -rw-r--r-- | lib/options.mli | 1 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 2 | ||||
| -rw-r--r-- | toplevel/toplevel.ml | 25 |
4 files changed, 23 insertions, 6 deletions
diff --git a/lib/options.ml b/lib/options.ml index b2f2943aa6..e59a19bbb7 100644 --- a/lib/options.ml +++ b/lib/options.ml @@ -22,6 +22,7 @@ let batch_mode = ref false let debug = ref false let print_emacs = ref false +let print_emacs_safechar = ref false let term_quality = ref false diff --git a/lib/options.mli b/lib/options.mli index 9fa408d921..7fa55e6367 100644 --- a/lib/options.mli +++ b/lib/options.mli @@ -17,6 +17,7 @@ val batch_mode : bool ref val debug : bool ref val print_emacs : bool ref +val print_emacs_safechar : bool ref val term_quality : bool ref diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index dada1ed9d3..763ed91f12 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -247,6 +247,8 @@ let parse_args is_ide = | "-vm" :: rem -> use_vm := true; parse rem | "-emacs" :: rem -> Options.print_emacs := true; Pp.make_pp_emacs(); parse rem + | "-emacs-U" :: rem -> Options.print_emacs := true; + Options.print_emacs_safechar := true; Pp.make_pp_emacs(); parse rem | "-where" :: _ -> print_endline (getenv_else "COQLIB" Coq_config.coqlib); exit 0 diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 7b4af1006e..3b96ede0b5 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -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 @@ -214,14 +222,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 +242,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. *) |