diff options
Diffstat (limited to 'otherlibs/labltk/browser/jg_message.ml')
| -rw-r--r-- | otherlibs/labltk/browser/jg_message.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/otherlibs/labltk/browser/jg_message.ml b/otherlibs/labltk/browser/jg_message.ml index 97a90bf9f3..6e15a4992f 100644 --- a/otherlibs/labltk/browser/jg_message.ml +++ b/otherlibs/labltk/browser/jg_message.ml @@ -13,6 +13,7 @@ (* $Id$ *) +open StdLabels open Tk open Jg_tk @@ -59,11 +60,12 @@ let formatted ~title ?on ?(ppf = Format.std_formatter) Format.pp_set_margin ppf (width - 2); let fof,fff = Format.pp_get_formatter_output_functions ppf () in Format.pp_set_formatter_output_functions ppf - ~out:(Jg_text.output tw) ~flush:(fun () -> ()); + (fun buf pos len -> Jg_text.output tw ~buf ~pos ~len) + ignore; tl, tw, begin fun () -> Format.pp_print_flush ppf (); - Format.pp_set_formatter_output_functions ppf ~out:fof ~flush:fff; + Format.pp_set_formatter_output_functions ppf fof fff; let `Linechar (l, _) = Text.index tw ~index:(tposend 1) in Text.configure tw ~height:(max minheight (min l maxheight)); if l > 5 then |