From: Claudio Sacerdoti Coen Date: Fri, 8 Jun 2012 08:59:06 +0000 (+0000) Subject: Msg reporting via HLogger in the error window made asynchronous => speedup. X-Git-Tag: make_still_working~1649 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0460fd3dc2909efe0baa6592281d0cf0527165ff;p=helm.git Msg reporting via HLogger in the error window made asynchronous => speedup. --- diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml index d009a63f6..0ecede622 100644 --- a/matita/matita/matitaGui.ml +++ b/matita/matita/matitaGui.ml @@ -774,7 +774,7 @@ class gui () = main#unicodeAsTexMenuItem#set_active (Helm_registry.get_bool "matita.paste_unicode_as_tex"); (* log *) - HLog.set_log_callback self#console#log_callback; + HLog.set_log_callback (fun tag msg -> GtkThread.async (self#console#log_callback tag) msg); GtkSignal.user_handler := (function | MatitaScript.ActionCancelled s -> HLog.error s