Ctr-C now is equivalent to pressing the Break button

[helm.git] / matita / matita / matitaGui.ml

diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml
index ee268e60add67ea6c06217317c37ebcefc340e90..af5ea58054d29dc014dd7befb4c33013a7447de7 100644 (file)
--- 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 =
@@ -652,6 +652,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 ()
@@ -718,7 +719,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 +787,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 +990,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 +1014,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 +1136,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 +1261,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 *)