diff options
author | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2014-12-15 20:56:07 +0100 |
---|---|---|
committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2014-12-15 20:56:15 +0100 |
commit | 0e730e4fa316cbfbd2d6dc60276498f57f500e0e (patch) | |
tree | a3149569f71bdc4ee842ec49b8d6d98c126c7102 /lib/pp.ml | |
parent | 594d2b8beb98b67f059014c5d76ba0d09dba2e4c (diff) |
Changed bullet informations to warning for better display in PG.
Since it displays together with the goal, it is better (for pg and
other interfaces probably) that they are in a different message.
Diffstat (limited to 'lib/pp.ml')
-rw-r--r-- | lib/pp.ml | 4 |
1 files changed, 4 insertions, 0 deletions
@@ -447,6 +447,10 @@ let logger = ref std_logger let feedback_id = ref (Feedback.Edit 0) let feedback_route = ref Feedback.default_route +(* If mixing some output and a goal display, please use msg_warning, + so that interfaces (proofgeneral for example) can easily dispatch + them to different windows. *) + let msg_info x = !logger ~id:!feedback_id Info x let msg_notice x = !logger ~id:!feedback_id Notice x let msg_warning x = !logger ~id:!feedback_id Warning x |