diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-05-18 07:31:36 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-01 15:50:26 +0200 |
commit | 6b041a242607ec906fbab451e53c15af6339e4ef (patch) | |
tree | ac7b4e6a25c0607c1770da551ed4f5de4addb310 /toplevel | |
parent | f3a388baf9cf2a14a658cab77554a0802b999486 (diff) |
[emacs] [toplevel] Make emacs flag local to the toplevel.
We remove the emacs-specific printing code from the core of Coq, now
`-emacs` is a printing flag controlled by the toplevel.
Diffstat (limited to 'toplevel')
-rw-r--r-- | toplevel/coqloop.ml | 15 | ||||
-rw-r--r-- | toplevel/coqloop.mli | 3 | ||||
-rw-r--r-- | toplevel/coqtop.ml | 6 |
3 files changed, 14 insertions, 10 deletions
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index ab5104c78..8806c7356 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -8,6 +8,8 @@ open Pp +let print_emacs = ref false + let top_stderr x = Format.fprintf !Topfmt.err_ft "@[%a@]%!" pp_with x @@ -45,9 +47,8 @@ let resynch_buffer ibuf = (* 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_endstring() = Printer.emacs_str "</prompt>" +let emacs_prompt_startstring () = if !print_emacs then "<prompt>" else "" +let emacs_prompt_endstring () = if !print_emacs then "</prompt>" else "" (* Read a char in an input channel, displaying a prompt at every beginning of line. *) @@ -56,7 +57,7 @@ let prompt_char ic ibuf count = | ll::_ -> Int.equal ibuf.len ll | [] -> Int.equal ibuf.len 0 in - if bol && not !Flags.print_emacs then top_stderr (str (ibuf.prompt())); + if bol && not !print_emacs then top_stderr (str (ibuf.prompt())); try let c = input_char ic in if c == '\n' then ibuf.bols <- (ibuf.len+1) :: ibuf.bols; @@ -168,7 +169,7 @@ let error_info_for_buffer ?loc buf = (* Actual printing routine *) let print_error_for_buffer ?loc lvl msg buf = let pre_hdr = error_info_for_buffer ?loc buf in - if !Flags.print_emacs + if !print_emacs then Topfmt.emacs_logger ?pre_hdr lvl msg else Topfmt.std_logger ?pre_hdr lvl msg @@ -207,7 +208,7 @@ let make_emacs_prompt() = (fun acc x -> acc ^ (if CString.is_empty acc then "" else "|") ^ Names.Id.to_string x) "" pending in let proof_info = if dpth >= 0 then string_of_int dpth else "0" in - if !Flags.print_emacs then statnum ^ " |" ^ pendingprompt ^ "| " ^ proof_info ^ " < " + if !print_emacs then statnum ^ " |" ^ pendingprompt ^ "| " ^ proof_info ^ " < " else "" (* A buffer to store the current command read on stdin. It is @@ -299,7 +300,7 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in let do_vernac sid = top_stderr (fnl()); - if !Flags.print_emacs then top_stderr (str (top_buffer.prompt())); + if !print_emacs then top_stderr (str (top_buffer.prompt())); resynch_buffer top_buffer; try let input = (top_buffer.tokens, None) in diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli index 13e860a88..a0e2f1e02 100644 --- a/toplevel/coqloop.mli +++ b/toplevel/coqloop.mli @@ -8,6 +8,9 @@ (** The Coq toplevel loop. *) +(** -emacs option: printing includes emacs tags. *) +val print_emacs : bool ref + (** A buffer for the character read from a channel. We store the command * entered to be able to report errors without pretty-printing. *) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 7834b5113..26ee413fb 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -246,21 +246,21 @@ let compile_files () = let set_emacs () = if not (Option.is_empty !toploop) then user_err Pp.(str "Flag -emacs is incompatible with a custom toplevel loop"); - Flags.print_emacs := true; + Coqloop.print_emacs := true; Printer.enable_goal_tags_printing := true; color := `OFF (** Options for CoqIDE *) let set_ideslave () = - if !Flags.print_emacs then user_err Pp.(str "Flags -ideslave and -emacs are incompatible"); + if !Coqloop.print_emacs then user_err Pp.(str "Flags -ideslave and -emacs are incompatible"); toploop := Some "coqidetop"; Flags.ide_slave := true (** Options for slaves *) let set_toploop name = - if !Flags.print_emacs then user_err Pp.(str "Flags -toploop and -emacs are incompatible"); + if !Coqloop.print_emacs then user_err Pp.(str "Flags -toploop and -emacs are incompatible"); toploop := Some name (** GC tweaking *) |