From 91ee24b4a7843793a84950379277d92992ba1651 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 11 Feb 2016 02:13:30 +0100 Subject: 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. --- kernel/nativelib.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'kernel/nativelib.ml') diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 4296b73ab..5b92e9554 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -73,20 +73,20 @@ let call_compiler ml_filename = ::"-w"::"a" ::include_dirs @ ["-impl"; ml_filename] in - if !Flags.debug then Pp.msg_debug (Pp.str (ocamlfind () ^ " " ^ (String.concat " " args))); + if !Flags.debug then Feedback.msg_debug (Pp.str (ocamlfind () ^ " " ^ (String.concat " " args))); try let res = CUnix.sys_command (ocamlfind ()) args in let res = match res with | Unix.WEXITED 0 -> true | Unix.WEXITED n -> - Pp.(msg_warning (str "command exited with status " ++ int n)); false + Feedback.msg_warning Pp.(str "command exited with status " ++ int n); false | Unix.WSIGNALED n -> - Pp.(msg_warning (str "command killed by signal " ++ int n)); false + Feedback.msg_warning Pp.(str "command killed by signal " ++ int n); false | Unix.WSTOPPED n -> - Pp.(msg_warning (str "command stopped by signal " ++ int n)); false in + Feedback.msg_warning Pp.(str "command stopped by signal " ++ int n); false in res, link_filename with Unix.Unix_error (e,_,_) -> - Pp.(msg_warning (str (Unix.error_message e))); + Feedback.msg_warning Pp.(str (Unix.error_message e)); false, link_filename let compile fn code = @@ -120,7 +120,7 @@ let call_linker ?(fatal=true) prefix f upds = begin let msg = "Cannot find native compiler file " ^ f in if fatal then Errors.error msg - else if !Flags.debug then Pp.msg_debug (Pp.str msg) + else if !Flags.debug then Feedback.msg_debug (Pp.str msg) end else (try @@ -129,8 +129,8 @@ let call_linker ?(fatal=true) prefix f upds = with Dynlink.Error e as exn -> let exn = Errors.push exn in let msg = "Dynlink error, " ^ Dynlink.error_message e in - if fatal then (Pp.msg_error (Pp.str msg); iraise exn) - else if !Flags.debug then Pp.msg_debug (Pp.str msg)); + if fatal then (Feedback.msg_error (Pp.str msg); iraise exn) + else if !Flags.debug then Feedback.msg_debug (Pp.str msg)); match upds with Some upds -> update_locations upds | _ -> () let link_library ~prefix ~dirname ~basename = -- cgit v1.2.3