From 84cc672d70212e4f204bc2f43120ec4d82f9bcd9 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 7 Mar 2014 18:05:12 +0000 Subject: [PATCH] Code changed a bit to make it work as before with OCaml 4.0. Without this patch, the refresh of the textual widget (e.g. the update of the locked part) is not immediately done. This is roughly the visual behaviour the user expects. On the other hand, we also expect the threads that execute and that responsible for the UI to work in parallel, which is not the case. The code I just touched stops the worker thread for, on average, 0.1s per tactic, which is really a lot. Switching to a multiprocess implementation (in place of a multithread) does not seem easy. Bad OCaml, bad. --- matita/matita/matitaScript.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index 6a03e3538..cb443ae46 100644 --- a/matita/matita/matitaScript.ml +++ b/matita/matita/matitaScript.ml @@ -776,7 +776,10 @@ object (self) buffer#move_mark mark mark_position; source_view#scroll_to_mark ~use_align:true ~xalign:1.0 ~yalign:0.1 mark; end; - while Glib.Main.pending () do ignore(Glib.Main.iteration false); done + let time0 = Unix.gettimeofday () in + GtkThread.sync (fun () -> while Glib.Main.pending () do ignore(Glib.Main.iteration false); done) (); + let time1 = Unix.gettimeofday () in + HLog.debug ("... refresh done in " ^ string_of_float (time1 -. time0) ^ "s") method clean_dirty_lock = let lock_mark_iter = buffer#get_iter_at_mark (`MARK locked_mark) in -- 2.39.2