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
String.concat "\n"
("" ::
List.map
- (fun k,desc ->
+ (fun (k,desc) ->
let alias =
match k with
| DisambiguateTypes.Id id ->
dialog#toplevel#destroy ()
) ()
+let ref_kill_worker = ref (fun _ -> assert false)
+
class gui () =
(* creation order _is_ relevant for windows placement *)
let main = new mainWin () in
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
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 *)
projects / helm.git / blobdiff