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

1 files changed, 11 insertions, 5 deletions

diff --git a/parsing/printer.mli b/parsing/printer.mli
index b4e0537a5e..cdd2f42770 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -115,11 +115,17 @@ val pr_evars_int           : int -> (evar * evar_info) list -> std_ppcmds
 val pr_prim_rule           : prim_rule -> std_ppcmds
 
 (** Emacs/proof general support 
-   (emacs_str s alts) outputs
-   - s if emacs mode & unicode allowed,
-   - alts if emacs mode and & unicode not allowed
-   - nothing otherwise *)
-val emacs_str              : string -> string -> string
+   (emacs_str s) outputs
+    - s if emacs mode,
+    - nothing otherwise.
+    This function was previously used to insert special chars like
+    [(String.make 1 (Char.chr 253))] to parenthesize sub-parts of the
+    proof context for proof by pointing. This part of the code is
+    removed for now because it interacted badly with utf8. We may put
+    it back some day using some xml-like tags instead of special
+    chars. See for example the <prompt> tag in the prompt when in
+    emacs mode. *)
+val emacs_str              : string -> string
 
 (** Backwards compatibility *)