X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;fp=helm%2Fmatita%2FmatitaGui.ml;h=853168b29cb49939d45fbc513b71889ab94d60fc;hb=78cd354ba5225f6431ab0bab6dcaa548bb5a24c3;hp=fe113743b1d0ef7d9cbe7d2e5b9ccf5cd282c98e;hpb=bc504bdaca501cd4d33f3240e01855988bc15b79;p=helm.git

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index fe113743b..853168b29 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -574,7 +574,35 @@ class gui () =
       GtkSignal.user_handler :=
         (fun exn ->
           if not (Helm_registry.get_bool "matita.debug") then
-            MatitaLog.error (MatitaExcPp.to_string exn)
+           let floc, msg = MatitaExcPp.to_string exn in
+            begin
+             match floc with
+                None -> ()
+              | Some floc ->
+                 let (x, y) = HExtlib.loc_of_floc floc in
+                 let script = MatitaScript.current () in
+                 let locked_mark = script#locked_mark in
+                 let error_tag = script#error_tag in
+                 let baseoffset =
+                  (source_buffer#get_iter_at_mark (`MARK locked_mark))#offset in
+                 let x' = baseoffset + x in
+                 let y' = baseoffset + y in
+                 let x_iter = source_buffer#get_iter (`OFFSET x') in
+                 let y_iter = source_buffer#get_iter (`OFFSET y') in
+                 source_buffer#apply_tag error_tag ~start:x_iter ~stop:y_iter;
+                 let id = ref None in
+                 id := Some (source_buffer#connect#changed ~callback:(fun () ->
+                   source_buffer#remove_tag error_tag
+                     ~start:source_buffer#start_iter
+                     ~stop:source_buffer#end_iter;
+                   match !id with
+                   | None -> assert false (* a race condition occurred *)
+                   | Some id ->
+                       (new GObj.gobject_ops source_buffer#as_buffer)#disconnect id));
+                 source_buffer#place_cursor
+                  (source_buffer#get_iter (`OFFSET x'));
+            end;
+            MatitaLog.error msg
           else raise exn);
         (* script *)
       ignore (source_buffer#connect#mark_set (fun _ _ -> next_ligatures <- []));