diff options
| author | Enrico Tassi | 2014-07-10 15:47:50 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2014-07-11 10:15:06 +0200 |
| commit | 024c980ab64e0d1102a10fdd793339c1dc84ac0f (patch) | |
| tree | 3aa917176e8b772111d7f6f1647934652695d8ae /lib/pp.mli | |
| parent | 39ef54919006741dba7c1860524b6800eb97a2c4 (diff) | |
make the standard logging facility stm aware
Diffstat (limited to 'lib/pp.mli')
| -rw-r--r-- | lib/pp.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/lib/pp.mli b/lib/pp.mli index fe11619c1d..ef7f6d11a2 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -115,6 +115,9 @@ val std_logger : logger val set_logger : logger -> unit +type modern_logger = id:Feedback.edit_or_state_id -> message_level -> std_ppcmds -> unit +val set_modern_logger : modern_logger -> unit + val of_message : message -> Xml_datatype.xml val to_message : Xml_datatype.xml -> message val is_message : Xml_datatype.xml -> bool |