diff options
| author |  courtieu <courtieu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-04-27 16:01:26 +0000 |
|---|---|---|
| committer | courtieu <courtieu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-04-27 16:01:26 +0000 |
| commit | d9e885515da1592075f5599290e6117c095216b4 (patch) | |
| tree | 8ffa7e3c045166abae5a46f8d83efa80dca1ee37 | |
| parent | c9f997fd32e3bccf58b9d3c26e1822a765c44d21 (diff) | |
Modification of emacs output: Pp.warning and al now output warning
between special characters.
I had to add a hidden variable print_emacs and a function to set it to
true in Pp because using Options.print_emacs would have introduce a
circularity.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8748 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | lib/pp.mli | 5 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 2 | ||||
| -rw-r--r-- | toplevel/toplevel.ml | 6 |
3 files changed, 10 insertions, 3 deletions
diff --git a/lib/pp.mli b/lib/pp.mli index 4e64925fd..d4248cc7f 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -12,6 +12,11 @@ open Pp_control (*i*) +(* Modify pretty printing functions behavior for emacs ouput (special + chars inserted at some places). This function should called once in + module [Options], that's all. *) +val make_pp_emacs:unit -> unit + (* Pretty-printers. *) type ppcmd diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 6e72dd63a..e74cad562 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -242,7 +242,7 @@ let parse_args is_ide = | "-debug" :: rem -> set_debug (); parse rem | "-vm" :: rem -> use_vm := true; parse rem - | "-emacs" :: rem -> Options.print_emacs := true; parse rem + | "-emacs" :: rem -> Options.print_emacs := true; Pp.make_pp_emacs(); parse rem | "-where" :: _ -> print_endline Coq_config.coqlib; exit 0 diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 9162c9fa7..7b4af1006 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -47,9 +47,12 @@ let resynch_buffer ibuf = ibuf.start <- ibuf.start + ll | _ -> () + (* Read a char in an input channel, displaying a prompt at every beginning of line. *) +let emacs_prompt_endstring = String.make 1 (Char.chr 249) + let prompt_char ic ibuf count = let bol = match ibuf.bols with | ll::_ -> ibuf.len == ll @@ -204,7 +207,6 @@ let make_prompt () = *) let make_emacs_prompt() = let statnum = string_of_int (Lib.current_command_label ()) in - let endchar = String.make 1 (Char.chr 249) in let dpth = Pfedit.current_proof_depth() in let pending = Pfedit.get_all_proof_names() in let pendingprompt = @@ -212,7 +214,7 @@ 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 ^ " < " ^ endchar + 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", |