X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaGui.ml;h=816dd3a303aa3d1f6c18c2f5e46ca74189048e33;hb=refs%2Fheads%2Fmaster;hp=ee268e60add67ea6c06217317c37ebcefc340e90;hpb=ad99cc72c725c0cceda7ddf3dbaafedfe4dcb5b2;p=helm.git diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml index ee268e60a..816dd3a30 100644 --- a/matita/matita/matitaGui.ml +++ b/matita/matita/matitaGui.ml @@ -31,8 +31,6 @@ open MatitaGeneratedGui open MatitaGtkMisc open MatitaMisc -exception Found of int - let all_disambiguation_passes = ref false (* this is a shit and should be changed :-{ *) @@ -41,7 +39,7 @@ let interactive_uri_choice ?(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") @@ -171,7 +169,7 @@ class interpErrorModel = 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 @@ -180,7 +178,7 @@ class interpErrorModel = (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" ^ @@ -198,7 +196,7 @@ class interpErrorModel = 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 @@ -377,7 +375,7 @@ let interactive_error_interp ~all_passes String.concat "\n" ("" :: List.map - (fun k,desc -> + (fun (k,desc) -> let alias = match k with | DisambiguateTypes.Id id -> @@ -402,6 +400,8 @@ let interactive_error_interp ~all_passes 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 @@ -554,15 +554,15 @@ class gui () = 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 = @@ -599,6 +599,7 @@ class gui () = 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 @@ -630,18 +631,21 @@ class gui () = 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 @@ -652,6 +656,7 @@ class gui () = 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 () @@ -665,6 +670,7 @@ class gui () = 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 @@ -718,7 +724,6 @@ class gui () = "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 () @@ -787,6 +792,7 @@ class gui () = 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; @@ -989,6 +995,8 @@ class gui () = 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 @@ -1011,7 +1019,7 @@ class gui () = 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 @@ -1133,7 +1141,7 @@ class interpModel = 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 @@ -1258,7 +1266,7 @@ let interactive_interp_choice () text prefix_len 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 *)