(fun () -> develList#toplevel#misc#hide());
ignore(develList#toplevel#event#connect#delete
(fun _ -> develList#toplevel#misc#hide();true));
- let selected_devel = ref None in
connect_menu_item main#developmentsMenuItem
(fun () -> refresh_devels_win ();develList#toplevel#misc#show ());
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 <- []));
in
let loadScript () =
let script = s () in
- let status = script#status in
try
match self#chooseFile () with
| Some f ->
(selection_mode :> Gtk.Tags.selection_mode);
let model = new stringListModel dialog#uriChoiceTreeView in
let choices = ref None in
- let nonvars = ref false in
(match copy_cb with
| None -> ()
| Some cb ->
assert (choices <> []);
let dialog = gui#newRecordDialog () in
let model = new interpModel dialog#recordChoiceTreeView choices in
- let interp_len = List.length (List.hd choices) in
dialog#recordChoiceDialog#set_title "Interpretation choice";
dialog#recordChoiceDialogLabel#set_label "Choose an interpretation:";
let interp_no = ref None in