From 245ff83b44c373455592e2e2271a2a7a79610799 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 30 Dec 2022 21:31:23 +0100 Subject: [PATCH] Avoid race conditions (deadlocks) --- matita/matita/matitaGui.ml | 4 +--- matita/matita/matitaScript.ml | 3 ++- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml index 7e2b0401b..2a1381e3d 100644 --- a/matita/matita/matitaGui.ml +++ b/matita/matita/matitaGui.ml @@ -558,9 +558,7 @@ class gui () = let source_view = (s ())#source_view in main#buttonsToolbar#misc#set_sensitive true; main#scriptMenu#misc#set_sensitive true; - source_view#set_editable true; - (*The next line seems sufficient to avoid some unknown race condition *) - GtkThread.sync (fun () -> ()) () + source_view#set_editable true in let worker_thread = ref None in let notify_exn (source_view : GSourceView3.source_view) exn = diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index 240122134..711ac975a 100644 --- a/matita/matita/matitaScript.ml +++ b/matita/matita/matitaScript.ml @@ -773,7 +773,8 @@ object (self) | n (* when n < 0 *) -> current_mark_pos#backward_chars (abs n) in buffer#move_mark mark ~where:new_mark_pos; - buffer#apply_tag locked_tag ~start:buffer#start_iter ~stop:new_mark_pos; + (* CSC: the next line is required to avoid race conditions (deadlocks) *) + GtkThread.sync(fun () -> buffer#apply_tag locked_tag ~start:buffer#start_iter ~stop:new_mark_pos) (); buffer#move_mark `INSERT old_insert; let mark_position = buffer#get_iter_at_mark mark in if source_view#move_mark_onscreen mark then -- 2.39.2