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 <- []));