diff options
author | 2016-02-11 02:13:30 +0100 | |
---|---|---|
committer | 2016-05-31 09:38:57 +0200 | |
commit | 91ee24b4a7843793a84950379277d92992ba1651 (patch) | |
tree | f176a54110e5f394acee26351c079a395dbf6a10 /toplevel/coqloop.ml | |
parent | b994e3195d296e9d12c058127ced381976c3a49e (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.ml | 16 |
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 () |