open MatitaGtkMisc
open MatitaMisc
-exception Found of int
-
let all_disambiguation_passes = ref false
(* this is a shit and should be changed :-{ *)
?(msg = "") ?(nonvars_button = false) ?(hide_uri_entry=false)
?(hide_try=false) ?(ok_label="_Auto") ?(ok_action:[`SELECT|`AUTO] = `AUTO)
?copy_cb ()
- ~id uris
+ ~id:_ uris
=
if (selection_mode <> `SINGLE) &&
(Helm_registry.get_opt_default Helm_registry.get_bool ~default:true "matita.auto_disambiguation")
| uris -> return (Some (List.map NReference.reference_of_string uris)));
connect_button dialog#uriChoiceAbortButton (fun _ -> return None);
dialog#uriChoiceDialog#show ();
+ (* CSC: old Gtk2 code. Use #run instead. Look for similar code handling
+ other dialogs *)
GtkThread.main ();
(match !choices with
| None -> raise MatitaTypes.Cancel
tree_store#clear ();
let idx1 = ref ~-1 in
List.iter
- (fun _,lll ->
+ (fun (_,lll) ->
incr idx1;
let loc_row =
if List.length choices = 1 then
(let loc_row = tree_store#append () in
begin
match lll with
- [passes,envs_and_diffs,_,_] ->
+ [passes,_envs_and_diffs,_,_] ->
tree_store#set ~row:loc_row ~column:id_col
("Error location " ^ string_of_int (!idx1+1) ^
", error message " ^ string_of_int (!idx1+1) ^ ".1" ^
Some loc_row) in
let idx2 = ref ~-1 in
List.iter
- (fun passes,envs_and_diffs,_,_ ->
+ (fun (passes,envs_and_diffs,_,_) ->
incr idx2;
let msg_row =
if List.length lll = 1 then
(MultiPassDisambiguator.DisambiguationError
(offset,[[env,diff,lazy (loffset,Lazy.force msg),significant]]));
| _::_ ->
+ GtkThread.sync (fun _ ->
let dialog = new disambiguationErrors () in
- if all_passes then
- dialog#disambiguationErrorsMoreErrors#misc#set_sensitive false;
+ dialog#toplevel#add_button "Fix this interpretation" `OK;
+ dialog#toplevel#add_button "Close" `DELETE_EVENT;
+ if not all_passes then
+ dialog#toplevel#add_button "More errors" `HELP; (* HELP means MORE *)
let model = new interpErrorModel dialog#treeview choices in
dialog#disambiguationErrors#set_title "Disambiguation error";
dialog#disambiguationErrorsLabel#set_label
(MultiPassDisambiguator.DisambiguationError
(offset,[[env,diff,lazy(loffset,Lazy.force msg),significant]]))
));
- let return _ =
- dialog#disambiguationErrors#destroy ();
- GMain.Main.quit ()
+ (match GtkThread.sync dialog#toplevel#run () with
+ | `OK ->
+ let tree_path =
+ match fst (dialog#treeview#get_cursor ()) with
+ None -> assert false
+ | Some tp -> tp in
+ let idx1,idx2,idx3 = model#get_interp_no tree_path in
+ let diff =
+ match idx2,idx3 with
+ Some idx2, Some idx3 ->
+ let _,lll = List.nth choices idx1 in
+ let _,envs_and_diffs,_,_ = List.nth lll idx2 in
+ let _,_,diff = List.nth envs_and_diffs idx3 in
+ diff
+ | _,_ -> assert false
in
- let fail _ = return () in
- ignore(dialog#disambiguationErrors#event#connect#delete (fun _ -> true));
- connect_button dialog#disambiguationErrorsOkButton
- (fun _ ->
- let tree_path =
- match fst (dialog#treeview#get_cursor ()) with
- None -> assert false
- | Some tp -> tp in
- let idx1,idx2,idx3 = model#get_interp_no tree_path in
- let diff =
- match idx2,idx3 with
- Some idx2, Some idx3 ->
- let _,lll = List.nth choices idx1 in
- let _,envs_and_diffs,_,_ = List.nth lll idx2 in
- let _,_,diff = List.nth envs_and_diffs idx3 in
- diff
- | _,_ -> assert false
- in
- let newtxt =
- String.concat "\n"
- ("" ::
- List.map
- (fun k,desc ->
- let alias =
- match k with
- | DisambiguateTypes.Id id ->
- GrafiteAst.Ident_alias (id, desc)
- | DisambiguateTypes.Symbol (symb, i)->
- GrafiteAst.Symbol_alias (symb, i, desc)
- | DisambiguateTypes.Num i ->
- GrafiteAst.Number_alias (i, desc)
- in
- GrafiteAstPp.pp_alias alias)
- diff) ^ "\n"
- in
- source_buffer#insert
- ~iter:
- (source_buffer#get_iter_at_mark
- (`NAME "beginning_of_statement")) newtxt ;
- return ()
- );
- connect_button dialog#disambiguationErrorsMoreErrors
- (fun _ -> return () ; raise UseLibrary);
- connect_button dialog#disambiguationErrorsCancelButton fail;
- dialog#disambiguationErrors#show ();
- GtkThread.main ()
+ let newtxt =
+ String.concat "\n"
+ ("" ::
+ List.map
+ (fun (k,desc) ->
+ let alias =
+ match k with
+ | DisambiguateTypes.Id id ->
+ GrafiteAst.Ident_alias (id, desc)
+ | DisambiguateTypes.Symbol (symb, i)->
+ GrafiteAst.Symbol_alias (symb, i, desc)
+ | DisambiguateTypes.Num i ->
+ GrafiteAst.Number_alias (i, desc)
+ in
+ GrafiteAstPp.pp_alias alias)
+ diff) ^ "\n"
+ in
+ source_buffer#insert
+ ~iter:
+ (source_buffer#get_iter_at_mark
+ (`NAME "beginning_of_statement")) newtxt
+ | `HELP (* HELP MEANS MORE *) ->
+ dialog#toplevel#destroy () ;
+ raise UseLibrary
+ | `DELETE_EVENT -> ()
+ | _ -> assert false) ;
+ dialog#toplevel#destroy ()
+ ) ()
+let ref_kill_worker = ref (fun _ -> assert false)
class gui () =
(* creation order _is_ relevant for windows placement *)
let source_view = (s ())#source_view in
main#buttonsToolbar#misc#set_sensitive false;
main#scriptMenu#misc#set_sensitive false;
- source_view#set_editable false
+ source_view#set_editable false;
+ main#scriptAbortButton#set_sensitive true
in
let unlock_world _ =
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 () -> ()) ()
+ main#scriptAbortButton#set_sensitive false
in
let worker_thread = ref None in
let notify_exn (source_view : GSourceView3.source_view) exn =
let source_view = script#source_view in
let thread_main =
fun () ->
+ ignore (Thread.sigmask Unix.SIG_UNBLOCK [Sys.sigvtalrm]);
lock_world ();
let saved_use_library= !MultiPassDisambiguator.use_library in
try
with Sys.Break as e -> notify_exn source_view e);
unlock_world ()
in
- (*thread_main ();*)
worker_thread := Some (Thread.create thread_main ())
in
let kill_worker =
- (* the following lines are from Xavier Leroy: http://alan.petitepomme.net/cwn/2005.11.08.html *)
let interrupt = ref None in
let old_callback = ref (function _ -> ()) in
let force_interrupt n =
- (* This function is called just before the thread's timeslice ends *)
+ (* This function is called every 1s (see Unix.setitimer call above) *)
!old_callback n;
+ (* it may be a masked interrupt for the previous thread that arrives
+ late *)
if Some(Thread.id(Thread.self())) = !interrupt then
- (interrupt := None; raise Sys.Break) in
+ (interrupt := None; raise Sys.Break)
+ in
+ ignore (Thread.sigmask Unix.SIG_BLOCK [Sys.sigvtalrm]);
+ ignore (Unix.setitimer Unix.ITIMER_VIRTUAL {Unix.it_interval = 1.; it_value = 1.});
let _ =
match Sys.signal Sys.sigvtalrm (Sys.Signal_handle force_interrupt) with
Sys.Signal_handle f -> old_callback := f
match !worker_thread with
None -> assert false
| Some t -> interrupt := Some (Thread.id t) in
+ ref_kill_worker := kill_worker ;
let keep_focus f (script: MatitaScript.script) =
try
f script; script#source_view#misc#grab_focus ()
ignore (adj#connect#changed
(fun _ -> adj#set_value (adj#upper -. adj#page_size)));
console#message (sprintf "\tMatita version %s\n" BuildTimeConf.version);
+ console#message (sprintf "\tStandard library location:\n\t %s\n" BuildTimeConf.new_stdlib_dir_devel);
(* natural deduction palette *)
main#tacticsButtonsHandlebox#misc#hide ();
MatitaGtkMisc.toggle_callback
"apply rule (∃#e (…) {…} […] (…));\n\t[\n\t|\n\t]\n");
- let module Hr = Helm_registry in
MatitaGtkMisc.toggle_callback ~check:main#fullscreenMenuItem
~callback:(function
| true -> main#toplevel#fullscreen ()
connect_button main#scriptBottomButton bottom;
connect_button main#scriptJumpButton jump;
connect_button main#scriptAbortButton kill_worker;
+ main#scriptAbortButton#set_sensitive false;
connect_menu_item main#scriptAdvanceMenuItem advance;
connect_menu_item main#scriptRetractMenuItem retract;
connect_menu_item main#scriptTopMenuItem top;
save_moo script#status;
true
| `NO -> true
- | `CANCEL -> false
+ | `DELETE_EVENT -> false
else
(save_moo script#status; true)
script#addObserver sequents_observer;
script#addObserver browser_observer
+ method kill_worker () = !ref_kill_worker ()
+
method loadScript file =
let page = main#scriptNotebook#current_page in
let script = MatitaScript.at_page page in
console#message ("'"^file^"' loaded.");
self#_enableSaveTo file
- method private _enableSaveTo file =
+ method private _enableSaveTo _file =
self#main#saveMenuItem#misc#set_sensitive true
method private console = console
let interactive_string_choice
- text prefix_len ?(title = "") ?(msg = "") () ~id locs uris
+ text prefix_len ?(title = "") ?msg:(_ = "") () ~id:_ locs uris
=
+ GtkThread.sync (fun _ ->
let dialog = new uriChoiceDialog () in
dialog#uriEntryHBox#misc#hide ();
dialog#uriChoiceSelectedButton#misc#hide ();
dialog#uriChoiceTreeView#selection#set_mode
(`SINGLE :> Gtk.Tags.selection_mode);
let model = new stringListModel dialog#uriChoiceTreeView in
- let choices = ref None in
+ let choices = ref [] in
dialog#uriChoiceDialog#set_title title;
let hack_len = MatitaGtkMisc.utf8_string_length text in
let rec colorize acc_len = function
in
dialog#uriChoiceLabel#set_label txt;
List.iter model#easy_append uris;
- let return v =
- choices := v;
- dialog#uriChoiceDialog#destroy ();
- GMain.Main.quit ()
- in
- ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true));
connect_button dialog#uriChoiceForwardButton (fun _ ->
match model#easy_selection () with
| [] -> ()
- | uris -> return (Some uris));
- connect_button dialog#uriChoiceAbortButton (fun _ -> return None);
+ | uris -> choices := uris; dialog#toplevel#response `OK);
+ connect_button dialog#uriChoiceAbortButton (fun _ -> dialog#toplevel#response `DELETE_EVENT);
dialog#uriChoiceDialog#show ();
- GtkThread.main ();
- (match !choices with
- | None -> raise MatitaTypes.Cancel
- | Some uris -> uris)
+ let res =
+ match dialog#toplevel#run () with
+ | `DELETE_EVENT -> dialog#toplevel#destroy() ; raise MatitaTypes.Cancel
+ | `OK -> !choices
+ | _ -> assert false in
+ dialog#toplevel#destroy () ;
+ res) ()
let interactive_interp_choice () text prefix_len choices =
(*List.iter (fun l -> prerr_endline "==="; List.iter (fun (_,id,dsc) -> prerr_endline (id ^ " = " ^ dsc)) l) choices;*)
let _ =
(* disambiguator callbacks *)
Disambiguate.set_choose_uris_callback
- (fun ~selection_mode ?ok ?(enable_button_for_non_vars=false) ~title ~msg ->
+ (fun ~selection_mode ?ok ?enable_button_for_non_vars:(_=false) ~title ~msg ->
interactive_uri_choice ~selection_mode ?ok_label:ok ~title ~msg ());
Disambiguate.set_choose_interp_callback (interactive_interp_choice ());
(* gtk initialization *)