diff options
| author | courtieu | 2011-05-24 19:01:42 +0000 |
|---|---|---|
| committer | courtieu | 2011-05-24 19:01:42 +0000 |
| commit | 77f1db2c35d3d337f4a47dc98d02f3c4749d9ade (patch) | |
| tree | a591fc7c1e0730f3489ff156a9b650a7da8d3d95 /toplevel | |
| parent | 4b0102ef92f22b9f81a2b8fb3fa72a5c434f3cfe (diff) | |
Made the emacs-U option deprecated. Also removed the old code
inserting special chars for proof by pointing with emacs. This was
interacting badly with utf8. It may be implemented back with xml-like
tags instead of special chars.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14154 85f007b7-540e-0410-9357-904b9bb8a0f7
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. *) |