diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 5 | ||||
| -rw-r--r-- | toplevel/toplevel.ml | 9 |
2 files changed, 7 insertions, 7 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index c0f6894674..eda05350b8 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -247,8 +247,9 @@ let parse_args arglist = | "-vm" :: rem -> use_vm := true; parse rem | "-emacs" :: rem -> Flags.print_emacs := true; Pp.make_pp_emacs(); parse rem - | "-emacs-U" :: rem -> Flags.print_emacs := true; - Flags.print_emacs_safechar := true; Pp.make_pp_emacs(); parse rem + | "-emacs-U" :: rem -> + warning "Obsolete option \"-emacs-U\", use -emacs instead."; + Flags.print_emacs := true; Pp.make_pp_emacs(); parse rem | "-unicode" :: rem -> add_require "Utf8_core"; parse rem diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 92e29c0421..699fd12f9d 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -47,13 +47,12 @@ let resynch_buffer ibuf = | _ -> () -(* 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. *) +(* emacs special prompt tag for easy detection. No special character, + to avoid interfering with utf8. Compatibility code removed. *) -let emacs_prompt_startstring() = Printer.emacs_str "" "<prompt>" +let emacs_prompt_startstring() = Printer.emacs_str "<prompt>" -let emacs_prompt_endstring() = Printer.emacs_str (String.make 1 (Char.chr 249)) "</prompt>" +let emacs_prompt_endstring() = Printer.emacs_str "</prompt>" (* Read a char in an input channel, displaying a prompt at every beginning of line. *) |