aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqloop.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2016-02-11 02:13:30 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2016-05-31 09:38:57 +0200
commit91ee24b4a7843793a84950379277d92992ba1651 (patch)
treef176a54110e5f394acee26351c079a395dbf6a10 /toplevel/coqloop.ml
parentb994e3195d296e9d12c058127ced381976c3a49e (diff)
Feedback cleanup
This patch splits pretty printing representation from IO operations. - `Pp` is kept in charge of the abstract pretty printing representation. - The `Feedback` module provides interface for doing printing IO. The patch continues work initiated for 8.5 and has the following effects: - The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`, `pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`, `msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be used instead. - Feedback provides different backends to handle output, currently, `stdout`, `emacs` and CoqIDE backends are provided. - Clients cannot specify flush policy anymore, thus `pp_flush` et al are gone. - `Feedback.feedback` takes an `edit_or_state_id` instead of the old mix. Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.
Diffstat (limited to 'toplevel/coqloop.ml')
-rw-r--r--toplevel/coqloop.ml16
1 files changed, 9 insertions, 7 deletions
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 040c33924..c8879963e 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -13,6 +13,8 @@ open Flags
open Vernac
open Pcoq
+let top_stderr x = msg_with !Pp_control.err_ft x
+
(* A buffer for the character read from a channel. We store the command
* entered to be able to report errors without pretty-printing. *)
@@ -59,7 +61,7 @@ let prompt_char ic ibuf count =
| ll::_ -> Int.equal ibuf.len ll
| [] -> Int.equal ibuf.len 0
in
- if bol && not !print_emacs then msgerr (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;
@@ -310,23 +312,23 @@ let read_sentence () =
*)
let do_vernac () =
- msgerrnl (mt ());
- if !print_emacs then msgerr (str (top_buffer.prompt()));
+ top_stderr (fnl());
+ if !print_emacs then top_stderr (str (top_buffer.prompt()));
resynch_buffer top_buffer;
try
Vernac.eval_expr (read_sentence ())
with
| End_of_input | Errors.Quit ->
- msgerrnl (mt ()); pp_flush(); raise Errors.Quit
+ top_stderr (fnl ()); raise Errors.Quit
| Errors.Drop -> (* Last chance *)
if Mltop.is_ocaml_top() then raise Errors.Drop
- else ppnl (str"Error: There is no ML toplevel." ++ fnl ())
+ else Feedback.msg_error (str"There is no ML toplevel.")
| any ->
let any = Errors.push any in
Format.set_formatter_out_channel stdout;
let msg = print_toplevel_error any ++ fnl () in
pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.std_ft msg;
- pp_flush ()
+ flush_all ()
(** Main coq loop : read vernacular expressions until Drop is entered.
Ctrl-C is handled internally as Sys.Break instead of aborting Coq.
@@ -354,7 +356,7 @@ let rec loop () =
| Errors.Drop -> ()
| Errors.Quit -> exit 0
| any ->
- msgerrnl (str"Anomaly: main loop exited with exception: " ++
+ Feedback.msg_error (str"Anomaly: main loop exited with exception: " ++
str (Printexc.to_string any) ++
fnl() ++ str"Please report.");
loop ()