diff -ur lablgtk-2.14.2.old/src/gtkThread.ml lablgtk-2.14.2/src/gtkThread.ml --- lablgtk-2.14.2.old/src/gtkThread.ml 2010-06-25 10:23:44.000000000 +0100 +++ lablgtk-2.14.2/src/gtkThread.ml 2011-07-27 19:16:32.263724495 +0100 @@ -28,8 +28,14 @@ let jobs : (unit -> unit) Queue.t = Queue.create () let m = Mutex.create () +type ('a, 'b) either = Left of 'a | Right of 'b let with_jobs f = - Mutex.lock m; let y = f jobs in Mutex.unlock m; y + Mutex.lock m; + let y = try Left (f jobs) with exn -> Right exn in + Mutex.unlock m; + match y with + | Left y -> y + | Right exn -> raise exn let loop_id = ref None let reset () = loop_id := None @@ -40,8 +46,6 @@ let gui_safe () = not (Sys.os_type = "Win32") || !loop_id = Some(Thread.id (Thread.self ())) -let has_jobs () = not (with_jobs Queue.is_empty) -let n_jobs () = with_jobs Queue.length let do_next_job () = with_jobs Queue.take () let async j x = with_jobs (Queue.add (fun () -> @@ -64,9 +68,9 @@ let do_jobs () = Thread.delay 0.0001; - for i = 1 to n_jobs () do do_next_job () done; + let rec loop () = do_next_job (); loop () in + (try loop () with Queue.Empty -> ()); true - (* We check first whether there are some event pending, and run some iterations. We then need to delay, thus focing a thread switch. *)