X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaGui.ml;h=ad34b7a5773c85aa87ee5bebe025f6e977ce0707;hb=ccf5878f2a2ec7f952f140e162391708a740517b;hp=e001f1db04661c8f9d884075e15c850b066f0037;hpb=6f24874d21e1ba9187599d0817c9ac8185a2464e;p=helm.git

diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml
index e001f1db0..ad34b7a57 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")
@@ -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" ^
@@ -318,11 +318,12 @@ let interactive_error_interp ~all_passes
           (MultiPassDisambiguator.DisambiguationError
             (offset,[[env,diff,lazy (loffset,Lazy.force msg),significant]]));
     | _::_ ->
+      GtkThread.sync (fun _ ->
        let dialog = new disambiguationErrors () in
-   dialog#toplevel#add_button "Fix this interpretation" `OK;
-   dialog#toplevel#add_button "Close" `DELETE_EVENT;
-   if not all_passes then
-    dialog#toplevel#add_button "More errors" `HELP; (* HELP means MORE *)
+       dialog#toplevel#add_button "Fix this interpretation" `OK;
+       dialog#toplevel#add_button "Close" `DELETE_EVENT;
+       if not all_passes then
+        dialog#toplevel#add_button "More errors" `HELP; (* HELP means MORE *)
        let model = new interpErrorModel dialog#treeview choices in
        dialog#disambiguationErrors#set_title "Disambiguation error";
        dialog#disambiguationErrorsLabel#set_label
@@ -354,8 +355,7 @@ let interactive_error_interp ~all_passes
             (MultiPassDisambiguator.DisambiguationError
               (offset,[[env,diff,lazy(loffset,Lazy.force msg),significant]]))
            ));
-   dialog#toplevel#show ();
-   ignore(dialog#toplevel#connect#response (function
+   (match GtkThread.sync dialog#toplevel#run () with
     | `OK ->
        let tree_path =
         match fst (dialog#treeview#get_cursor ()) with
@@ -391,13 +391,14 @@ let interactive_error_interp ~all_passes
          source_buffer#insert
           ~iter:
             (source_buffer#get_iter_at_mark
-             (`NAME "beginning_of_statement")) newtxt ;
-         dialog#toplevel#destroy ()
+             (`NAME "beginning_of_statement")) newtxt
     | `HELP (* HELP MEANS MORE *) ->
-        dialog#toplevel#destroy ();
+        dialog#toplevel#destroy () ;
         raise UseLibrary
-    | `DELETE_EVENT -> dialog#toplevel#destroy ()
-    | _ -> assert false))
+    | `DELETE_EVENT -> ()
+    | _ -> assert false) ;
+   dialog#toplevel#destroy ()
+  ) ()
 
 class gui () =
     (* creation order _is_ relevant for windows placement *)
@@ -928,7 +929,7 @@ class gui () =
              save_moo script#status;
              true
         | `NO -> true
-        | `CANCEL -> false
+        | `DELETE_EVENT -> false
       else 
        (save_moo script#status; true)
 
@@ -1008,7 +1009,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
@@ -1130,8 +1131,9 @@ 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
  dialog#uriEntryHBox#misc#hide ();
  dialog#uriChoiceSelectedButton#misc#hide ();
@@ -1140,7 +1142,7 @@ let interactive_string_choice
  dialog#uriChoiceTreeView#selection#set_mode
    (`SINGLE :> Gtk.Tags.selection_mode);
  let model = new stringListModel dialog#uriChoiceTreeView in
- let choices = ref None in
+ let choices = ref [] in
  dialog#uriChoiceDialog#set_title title; 
  let hack_len = MatitaGtkMisc.utf8_string_length text in
  let rec colorize acc_len = function
@@ -1175,22 +1177,19 @@ let interactive_string_choice
   in
   dialog#uriChoiceLabel#set_label txt;
   List.iter model#easy_append uris;
-  let return v =
-    choices := v;
-    dialog#uriChoiceDialog#destroy ();
-    GMain.Main.quit ()
-  in
-  ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true));
   connect_button dialog#uriChoiceForwardButton (fun _ ->
     match model#easy_selection () with
     | [] -> ()
-    | uris -> return (Some uris));
-  connect_button dialog#uriChoiceAbortButton (fun _ -> return None);
+    | uris -> choices := uris; dialog#toplevel#response `OK);
+  connect_button dialog#uriChoiceAbortButton (fun _ -> dialog#toplevel#response `DELETE_EVENT);
   dialog#uriChoiceDialog#show ();
-  GtkThread.main ();
-  (match !choices with 
-  | None -> raise MatitaTypes.Cancel
-  | Some uris -> uris)
+  let res =
+   match dialog#toplevel#run () with 
+    | `DELETE_EVENT -> dialog#toplevel#destroy() ; raise MatitaTypes.Cancel
+    | `OK -> !choices
+    | _ -> assert false in
+  dialog#toplevel#destroy () ;
+  res) ()
 
 let interactive_interp_choice () text prefix_len choices =
 (*List.iter (fun l -> prerr_endline "==="; List.iter (fun (_,id,dsc) -> prerr_endline (id ^ " = " ^ dsc)) l) choices;*)
@@ -1257,7 +1256,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 *)