diff options
| -rw-r--r-- | lib/pp.ml | 10 | ||||
| -rw-r--r-- | lib/pp.mli | 6 | ||||
| -rw-r--r-- | printing/printer.ml | 6 | ||||
| -rw-r--r-- | proofs/logic_monad.ml | 2 | ||||
| -rw-r--r-- | proofs/refiner.ml | 2 |
5 files changed, 17 insertions, 9 deletions
@@ -370,10 +370,17 @@ let pp_dirs ?pp_tag ft = let emacs_quote_start = String.make 1 (Char.chr 254) let emacs_quote_end = String.make 1 (Char.chr 255) +let emacs_quote_info_start = "<infomsg>" +let emacs_quote_info_end = "</infomsg>" + let emacs_quote g = if !print_emacs then str emacs_quote_start ++ hov 0 g ++ str emacs_quote_end else hov 0 g +let emacs_quote_info g = + if !print_emacs then str emacs_quote_info_start ++ hov 0 g ++ str emacs_quote_info_end + else hov 0 g + (* pretty printing functions WITHOUT FLUSH *) let pp_with ?pp_tag ft strm = @@ -434,10 +441,11 @@ let make_body info s = let debugbody strm = hov 0 (str "Debug:" ++ spc () ++ strm) let warnbody strm = make_body (str "Warning:") strm let errorbody strm = make_body (str "Error:") strm +let infobody strm = emacs_quote_info strm let std_logger ~id:_ level msg = match level with | Debug _ -> msgnl (debugbody msg) -| Info -> msgnl (hov 0 msg) +| Info -> msgnl (infobody (hov 0 msg)) | Notice -> msgnl msg | Warning -> Flags.if_warn (fun () -> msgnl_with !err_ft (warnbody msg)) () | Error -> msgnl_with !err_ft (errorbody msg) diff --git a/lib/pp.mli b/lib/pp.mli index d4314a336..9f65c0be0 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -124,9 +124,9 @@ type logger = message_level -> std_ppcmds -> unit (** {6 output functions} -[msg_info] and [msg_notice] do not put any decoration on output by -default. If possible don't mix them with goal output (prefer -msg_warning) so that dispatching of outputs is easier. Once all +[msg_notice] do not put any decoration on output by default. If +possible don't mix it with goal output (prefer msg_info or +msg_warning) so that interfaces can dispatch outputs easily. Once all interfaces use the xml-like protocol this constraint can be relaxed. *) (* Should we advertise these functions more? Should they be the ONLY diff --git a/printing/printer.ml b/printing/printer.ml index 5d9fa1313..7dfcde3ed 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -618,15 +618,15 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () = begin match bgoals,shelf,given_up with | [] , [] , [] -> pr_subgoals None sigma seeds shelf stack goals | [] , [] , _ -> - msg_warning (str "No more goals, however there are goals you gave up. You need to go back and solve them."); + msg_info (str "No more goals, however there are goals you gave up. You need to go back and solve them."); fnl () ++ fnl () ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] given_up | [] , _ , _ -> - msg_warning (str "All the remaining goals are on the shelf."); + msg_info (str "All the remaining goals are on the shelf."); fnl () ++ fnl () ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] shelf | _ , _, _ -> - msg_warning (str "This subproof is complete, but there are still unfocused goals."); + msg_info (str "This subproof is complete, but there are still unfocused goals."); fnl () ++ fnl () ++ pr_subgoals ~pr_first:false None bsigma seeds shelf [] bgoals end diff --git a/proofs/logic_monad.ml b/proofs/logic_monad.ml index 5bad5f0f5..b9c850840 100644 --- a/proofs/logic_monad.ml +++ b/proofs/logic_monad.ml @@ -95,7 +95,7 @@ struct let print_char = fun c -> (); fun () -> print_char c (** {!Pp.pp}. The buffer is also flushed. *) - let print = fun s -> (); fun () -> try Pp.pp s; Pp.pp_flush () with e -> + let print = fun s -> (); fun () -> try Pp.msg_info s; Pp.pp_flush () with e -> let (e, info) = Errors.push e in raise ~info e () let timeout = fun n t -> (); fun () -> diff --git a/proofs/refiner.ml b/proofs/refiner.ml index e443ce077..ea3594610 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -57,7 +57,7 @@ let tclIDTAC gls = goal_goal_list gls (* the message printing identity tactic *) let tclIDTAC_MESSAGE s gls = - pp (hov 0 s); pp_flush (); tclIDTAC gls + Pp.msg_info (hov 0 s); pp_flush (); tclIDTAC gls (* General failure tactic *) let tclFAIL_s s gls = errorlabstrm "Refiner.tclFAIL_s" (str s) |