let lock_world _ =
main#buttonsToolbar#misc#set_sensitive false;
develList#buttonsHbox#misc#set_sensitive false;
+ main#scriptMenu#misc#set_sensitive false;
source_view#set_editable false
in
let unlock_world _ =
main#buttonsToolbar#misc#set_sensitive true;
develList#buttonsHbox#misc#set_sensitive true;
+ main#scriptMenu#misc#set_sensitive true;
source_view#set_editable true
in
- let locker f =
+ 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
+ try f ();unlock_world () with exc -> unlock_world (); raise exc
+ 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 old_callback = ref (function _ -> ()) in
+ let force_interrupt n =
+ (* This function is called just before the thread's timeslice ends *)
+ !old_callback n;
+ if Some(Thread.id(Thread.self())) = !interrupt then
+ (interrupt := None; raise Sys.Break) in
+ let _ =
+ match Sys.signal Sys.sigvtalrm (Sys.Signal_handle force_interrupt) with
+ Sys.Signal_handle f -> old_callback := f
+ | Sys.Signal_ignore
+ | Sys.Signal_default -> assert false
+ in
+ fun () ->
+ match !worker_thread with
+ None -> assert false
+ | Some t -> interrupt := Some (Thread.id t) in
let keep_focus f =
fun () ->
try
match get_devel_selected () with
| None -> ()
| Some d ->
- let clean = locker
- (fun () -> MatitamakeLib.publish_development_in_bg refresh d)
- in
- ignore(clean ())));
+ let publish = locker (fun () ->
+ MatitamakeLib.publish_development_in_bg refresh d) in
+ ignore(publish ())));
+ connect_button develList#graphButton (fun () ->
+ match get_devel_selected () with
+ | None -> ()
+ | Some d ->
+ (match MatitamakeLib.dot_for_development d with
+ | None -> ()
+ | Some _ ->
+ let browser = MatitaMathView.cicBrowser () in
+ browser#load (`Development
+ (MatitamakeLib.name_for_development d))));
connect_button develList#closeButton
(fun () -> develList#toplevel#misc#hide());
ignore(develList#toplevel#event#connect#delete
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;
Helm_registry.get_opt_default Helm_registry.string ~default:"./"
"matita.tptppath"
in
- let data = Matitaprover.p_to_ma ~filename:file ~tptppath in
+ let data = Matitaprover.p_to_ma ~filename:file ~tptppath () in
let filename = Pcre.replace ~pat:"\\.p$" ~templ:".ma" file in
script#assignFileName filename;
source_view#source_buffer#begin_not_undoable_action ();