From 4f249fd1382d4124dc081b08d45c5f91f5134ffb Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 2 Oct 2006 17:44:01 +0000 Subject: [PATCH] This commit implements the Abort button for the GUI using a clever trick by Xavier Leroy. --- helm/software/matita/matita.glade | 490 +++++++++++++++++++++++------- helm/software/matita/matitaGui.ml | 16 +- 2 files changed, 402 insertions(+), 104 deletions(-) diff --git a/helm/software/matita/matita.glade b/helm/software/matita/matita.glade index 62d991dc2..415b3b308 100644 --- a/helm/software/matita/matita.glade +++ b/helm/software/matita/matita.glade @@ -2295,185 +2295,237 @@ 0 - + True - GTK_ORIENTATION_HORIZONTAL - GTK_TOOLBAR_BOTH - True - True + False + 0 - + True - True - True - False + GTK_ORIENTATION_HORIZONTAL + GTK_TOOLBAR_BOTH + True + True - + True - Restart - True - GTK_RELIEF_NONE - True + True + True + False - + True - gtk-goto-top - 4 - 0.5 - 0.5 - 0 - 0 + Restart + True + GTK_RELIEF_NONE + True + + + + True + gtk-goto-top + 4 + 0.5 + 0.5 + 0 + 0 + + + + False + False + - - - False - False - - - - - - True - True - True - False - + True - Retract 1 phrase - True - GTK_RELIEF_NONE - True + True + True + False - + True - gtk-go-up - 4 - 0.5 - 0.5 - 0 - 0 + Retract 1 phrase + True + GTK_RELIEF_NONE + True + + + + True + gtk-go-up + 4 + 0.5 + 0.5 + 0 + 0 + + + + False + False + - - - False - False - - - - - - True - True - True - False - + True - Execute until point - True - GTK_RELIEF_NONE - True + True + True + False - + True - gtk-jump-to - 4 - 0.5 - 0.5 - 0 - 0 + Execute until point + True + GTK_RELIEF_NONE + True + + + + True + gtk-jump-to + 4 + 0.5 + 0.5 + 0 + 0 + + + + False + False + - - - False - False - - - - - True - True - True - False + + + True + True + True + False + + + + True + Execute 1 phrase + True + GTK_RELIEF_NONE + True + + + + True + gtk-go-down + 4 + 0.5 + 0.5 + 0 + 0 + + + + + + + False + False + + - + True - Execute 1 phrase - True - GTK_RELIEF_NONE - True + True + True + False - + True - gtk-go-down - 4 - 0.5 - 0.5 - 0 - 0 + Execute all + True + GTK_RELIEF_NONE + True + + + + True + gtk-goto-bottom + 4 + 0.5 + 0.5 + 0 + 0 + + + + False + False + - False - False + 0 + True + True - + True True True False - + True - Execute all + Abort True GTK_RELIEF_NONE True - + True - gtk-goto-bottom + gtk-cancel 4 0.5 0.5 0 0 + + abort + + 0 False - False + False @@ -4333,4 +4385,236 @@ + + True + window1 + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_NONE + False + True + False + True + False + False + GDK_WINDOW_TYPE_HINT_NORMAL + GDK_GRAVITY_NORTH_WEST + True + False + + + + True + False + 0 + + + + True + GTK_ORIENTATION_HORIZONTAL + GTK_TOOLBAR_BOTH + True + True + + + + True + True + True + False + + + + True + Restart + True + GTK_RELIEF_NONE + True + + + + True + gtk-goto-top + 4 + 0.5 + 0.5 + 0 + 0 + + + + + + + False + False + + + + + + True + True + True + False + + + + True + Retract 1 phrase + True + GTK_RELIEF_NONE + True + + + + True + gtk-go-up + 4 + 0.5 + 0.5 + 0 + 0 + + + + + + + False + False + + + + + + True + True + True + False + + + + True + Execute until point + True + GTK_RELIEF_NONE + True + + + + True + gtk-jump-to + 4 + 0.5 + 0.5 + 0 + 0 + + + + + + + False + False + + + + + + True + True + True + False + + + + True + Execute 1 phrase + True + GTK_RELIEF_NONE + True + + + + True + gtk-go-down + 4 + 0.5 + 0.5 + 0 + 0 + + + + + + + False + False + + + + + + True + True + True + False + + + + True + Execute all + True + GTK_RELIEF_NONE + True + + + + True + gtk-goto-bottom + 4 + 0.5 + 0.5 + 0 + 0 + + + + + + + False + False + + + + + 0 + True + True + + + + + + True + gtk-cancel + 4 + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index af9984c1b..ed90fd29d 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -422,13 +422,26 @@ class gui () = develList#buttonsHbox#misc#set_sensitive true; source_view#set_editable true in + let worker_thread = ref None in let locker f () = let thread_main = fun () -> lock_world (); try f ();unlock_world () with exc -> unlock_world (); raise exc in - ignore (Thread.create thread_main ()) in + 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 force_interrupt n = + (* This function is called just before the thread's timeslice ends *) + if Some(Thread.id(Thread.self())) = !interrupt then + (interrupt := None; raise Sys.Break) in + let _ = Sys.signal Sys.sigvtalrm (Sys.Signal_handle force_interrupt) in + fun () -> + match !worker_thread with + None -> assert false + | Some t -> interrupt := Some (Thread.id t) in let keep_focus f = fun () -> try @@ -801,6 +814,7 @@ class gui () = connect_button main#scriptTopButton top; connect_button main#scriptBottomButton bottom; connect_button main#scriptJumpButton jump; + connect_button main#scriptAbortButton kill_worker; connect_menu_item main#scriptAdvanceMenuItem advance; connect_menu_item main#scriptRetractMenuItem retract; connect_menu_item main#scriptTopMenuItem top; -- 2.39.2