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
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;
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