Merge branch 'declarative' into matita-lablgtk3

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

diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml
index c1e8e9fc57d19dd92e31ec1d6ab5decdd78f5f63..5b7352d743f9cbaf4ade7b39b3af0cd85fb3cbe7 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")
@@ -97,6 +95,8 @@ let interactive_uri_choice
       | uris -> return (Some (List.map NReference.reference_of_string uris)));
     connect_button dialog#uriChoiceAbortButton (fun _ -> return None);
     dialog#uriChoiceDialog#show ();
+    (* CSC: old Gtk2 code. Use #run instead. Look for similar code handling
+       other dialogs *)
     GtkThread.main ();
     (match !choices with 
     | None -> raise MatitaTypes.Cancel
@@ -178,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" ^
@@ -601,11 +601,15 @@ class gui () =
           let saved_use_library= !MultiPassDisambiguator.use_library in
           try
            MultiPassDisambiguator.use_library := !all_disambiguation_passes;
+           prerr_endline "PRIMA";
            f script;
            MultiPassDisambiguator.use_library := saved_use_library;
-           unlock_world ()
+           prerr_endline "DOPO";
+           unlock_world () ;
+           prerr_endline "FINE";
           with
            | MultiPassDisambiguator.DisambiguationError (offset,errorll) ->
+              prerr_endline "EXC1";
               (try
                 interactive_error_interp 
                  ~all_passes:!all_disambiguation_passes source_view#source_buffer
@@ -622,7 +626,9 @@ class gui () =
                        notify_exn source_view exc);
                 | exc -> notify_exn source_view exc);
               MultiPassDisambiguator.use_library := saved_use_library;
-              unlock_world ()
+              prerr_endline "DOPO1";
+              unlock_world ();
+              prerr_endline "FINE1"
            | exc ->
               (try notify_exn source_view exc
                with Sys.Break as e -> notify_exn source_view e);
@@ -929,7 +935,7 @@ class gui () =
              save_moo script#status;
              true
         | `NO -> true
-        | `CANCEL -> false
+        | `DELETE_EVENT -> false
       else 
        (save_moo script#status; true)
 
@@ -1009,7 +1015,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
@@ -1131,7 +1137,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
@@ -1256,7 +1262,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 *)