diff --git a/src/kernel_services/plugin_entry_points/log.ml b/src/kernel_services/plugin_entry_points/log.ml index 9ac3d86df1daae9a76dbb69360fb26652a4fdc5c..aae66eac586ef30524b4a062ecc16adb150dd63e 100644 --- a/src/kernel_services/plugin_entry_points/log.ml +++ b/src/kernel_services/plugin_entry_points/log.ml @@ -419,17 +419,7 @@ let check_not_yet = ref (fun _evt -> false) (* --- Listeners --- *) (* -------------------------------------------------------------------------- *) -let firelock = ref false - -let do_fire e f = - if !firelock then f e else - try - firelock := true ; - f e ; - firelock := false - with exn -> - firelock := false ; - raise exn +let do_fire e f = f e let iter_kind ?kind f ems = match kind with @@ -490,6 +480,8 @@ let logtransient channel text = raise e ) buffer text +let locked_listeners = ref false + let logwithfinal finally channel ?(fire=true) (* fire channel listeners *) ?emitwith (* additional emitter *) @@ -528,8 +520,16 @@ let logwithfinal finally channel if echo && e.echo then do_echo channel.terminal event ; Extlib.may (do_fire event) emitwith; - if fire && not !firelock then - List.iter (do_fire event) e.listeners ; + if fire && not !locked_listeners then + begin + try + locked_listeners := true ; + List.iter (do_fire event) e.listeners ; + locked_listeners := false ; + with exn -> + locked_listeners := false ; + raise exn + end ; Some event end else None