The emacs-U option now does not output *any* char above 250.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9384 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 22 insertions, 18 deletions

diff --git a/parsing/printer.ml b/parsing/printer.ml
index a128eb1a71..deaf796ada 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -29,7 +29,11 @@ open Pfedit
 open Ppconstr
 open Constrextern
 
-let emacs_str s = if !Options.print_emacs then s else "" 
+let emacs_str s alts = 
+  match !Options.print_emacs, !Options.print_emacs_safechar with
+    | true, true -> alts
+    | true , false -> s
+    | false,_ -> "" 
 
 (**********************************************************************)
 (** Terms                                                             *)
@@ -210,7 +214,7 @@ let pr_context_limit n env =
 	   else
              let pidt = pr_var_decl env d in
 	     (i+1, (pps ++ fnl () ++
-		      str (emacs_str (String.make 1 (Char.chr 253))) ++
+		      str (emacs_str (String.make 1 (Char.chr 253)) "") ++
 		      pidt)))
         env ~init:(0,(mt ())) 
     in
@@ -219,7 +223,7 @@ let pr_context_limit n env =
         (fun env d pps ->
            let pnat = pr_rel_decl env d in
 	   (pps ++ fnl () ++
-	      str (emacs_str (String.make 1 (Char.chr 253))) ++
+	      str (emacs_str (String.make 1 (Char.chr 253)) "") ++
 	      pnat))
         env ~init:(mt ())
     in 
@@ -236,7 +240,7 @@ let pr_restricted_named_context among env =
 	  (fun env ((id,_,_) as d) pps ->
 	     if true || Idset.mem id among then
 	       pps ++ 
-		 fnl () ++ str (emacs_str (String.make 1 (Char.chr 253))) ++
+		 fnl () ++ str (emacs_str (String.make 1 (Char.chr 253)) "") ++
 		 pr_var_decl env d
 	     else 
 	       pps)
@@ -246,7 +250,7 @@ let pr_subgoal_metas metas env=
   let pr_one (meta,typ) = 
     str "?" ++ int meta ++ str " : " ++ 
       hov 0 (pr_ltype_env_at_top env typ) ++ fnl () ++ 
-      str (emacs_str (String.make 1 (Char.chr 253))) in
+      str (emacs_str (String.make 1 (Char.chr 253)) "") in
     hv 0 (prlist_with_sep mt pr_one metas)
 
 (* display complete goal *)
@@ -265,7 +269,7 @@ let pr_goal g =
   in
     preamb ++
     str"  " ++ hv 0 (penv ++ fnl () ++
-		       str (emacs_str (String.make 1 (Char.chr 253)))  ++
+		       str (emacs_str (String.make 1 (Char.chr 253)) "")  ++
 		       str "============================" ++ fnl ()  ++
 		       str" "  ++ pc) ++ fnl ()
      
@@ -273,7 +277,7 @@ let pr_goal g =
 let pr_concl n g =
   let env = evar_env g in
   let pc = pr_ltype_env_at_top env g.evar_concl in
-    str (emacs_str (String.make 1 (Char.chr 253)))  ++
+    str (emacs_str (String.make 1 (Char.chr 253)) "")  ++
       str "subgoal " ++ int n ++ str " is:" ++ cut () ++ str" "  ++ pc
 
 
diff --git a/parsing/printer.mli b/parsing/printer.mli
index dd2a7bad06..580eec8dc3 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -98,8 +98,11 @@ val pr_evars_int           : int -> (evar * evar_info) list -> std_ppcmds
 val pr_prim_rule           : prim_rule -> std_ppcmds
 
 (* Emacs/proof general support *)
-
-val emacs_str              : string -> string
+(* (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
 
 (* Backwards compatibility *)
 
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index ac8167f289..f75b8fc683 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -52,12 +52,9 @@ let resynch_buffer ibuf =
    (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_startstring() = Printer.emacs_str "" "<prompt>"
 
-let emacs_prompt_endstring() = 
-  if !Options.print_emacs_safechar then "</prompt>"
-  else String.make 1 (Char.chr 249)
+let emacs_prompt_endstring() = Printer.emacs_str (String.make 1 (Char.chr 249)) "</prompt>"
 
 (* Read a char in an input channel, displaying a prompt at every
    beginning of line. *)
@@ -230,9 +227,9 @@ let make_emacs_prompt() =
  * or after a Drop. *)
 let top_buffer =
   let pr() = 
-    Printer.emacs_str (emacs_prompt_startstring()) 
+    emacs_prompt_startstring() 
     ^ make_prompt() 
-    ^ Printer.emacs_str (make_emacs_prompt())
+    ^ make_emacs_prompt()
   in
   { prompt = pr;
     str = "";
@@ -244,9 +241,9 @@ let top_buffer =
 let set_prompt prompt =
   top_buffer.prompt
   <- (fun () -> 
-    Printer.emacs_str (emacs_prompt_startstring())
+    emacs_prompt_startstring()
     ^ prompt ()
-    ^ Printer.emacs_str (emacs_prompt_endstring()))
+    ^ emacs_prompt_endstring())
 
 (* Removes and prints the location of the error. The following exceptions
    need not be located. *)