Added a new option -emacs-U changing emacs prompt delimiters by

xml-like patterns (<prompt></prompt>).


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

4 files changed, 23 insertions, 6 deletions

diff --git a/lib/options.ml b/lib/options.ml
index b2f2943aa..e59a19bbb 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 9fa408d92..7fa55e636 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 dada1ed9d..763ed91f1 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 7b4af1006..3b96ede0b 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. *)