X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaGui.ml;h=ee268e60add67ea6c06217317c37ebcefc340e90;hb=cf8b1c25a0011ca2a8a856b39e046da33c451221;hp=d8de328ef17d5dad8ea13e94ec6aa2349075c21c;hpb=a823c605d3a541c8d7df2bcc3c21bf459c9d25c4;p=helm.git

diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml
index d8de328ef..ee268e60a 100644
--- a/matita/matita/matitaGui.ml
+++ b/matita/matita/matitaGui.ml
@@ -97,6 +97,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
@@ -318,9 +320,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
-       if all_passes then
-        dialog#disambiguationErrorsMoreErrors#misc#set_sensitive false;
+       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
@@ -352,57 +357,50 @@ let interactive_error_interp ~all_passes
             (MultiPassDisambiguator.DisambiguationError
               (offset,[[env,diff,lazy(loffset,Lazy.force msg),significant]]))
            ));
-       let return _ =
-         dialog#disambiguationErrors#destroy ();
-         GMain.Main.quit ()
+   (match GtkThread.sync dialog#toplevel#run () with
+    | `OK ->
+       let tree_path =
+        match fst (dialog#treeview#get_cursor ()) with
+           None -> assert false
+        | Some tp -> tp in
+       let idx1,idx2,idx3 = model#get_interp_no tree_path in
+       let diff =
+        match idx2,idx3 with
+           Some idx2, Some idx3 ->
+            let _,lll = List.nth choices idx1 in
+            let _,envs_and_diffs,_,_ = List.nth lll idx2 in
+            let _,_,diff = List.nth envs_and_diffs idx3 in
+             diff
+         | _,_ -> assert false
        in
-       let fail _ = return () in
-       ignore(dialog#disambiguationErrors#event#connect#delete (fun _ -> true));
-       connect_button dialog#disambiguationErrorsOkButton
-        (fun _ ->
-          let tree_path =
-           match fst (dialog#treeview#get_cursor ()) with
-              None -> assert false
-           | Some tp -> tp in
-          let idx1,idx2,idx3 = model#get_interp_no tree_path in
-          let diff =
-           match idx2,idx3 with
-              Some idx2, Some idx3 ->
-               let _,lll = List.nth choices idx1 in
-               let _,envs_and_diffs,_,_ = List.nth lll idx2 in
-               let _,_,diff = List.nth envs_and_diffs idx3 in
-                diff
-            | _,_ -> assert false
-          in
-           let newtxt =
-            String.concat "\n"
-             ("" ::
-               List.map
-                (fun k,desc -> 
-                  let alias =
-                   match k with
-                   | DisambiguateTypes.Id id ->
-                       GrafiteAst.Ident_alias (id, desc)
-                   | DisambiguateTypes.Symbol (symb, i)-> 
-                       GrafiteAst.Symbol_alias (symb, i, desc)
-                   | DisambiguateTypes.Num i ->
-                       GrafiteAst.Number_alias (i, desc)
-                  in
-                   GrafiteAstPp.pp_alias alias)
-                diff) ^ "\n"
-           in
-            source_buffer#insert
-             ~iter:
-               (source_buffer#get_iter_at_mark
-                (`NAME "beginning_of_statement")) newtxt ;
-            return ()
-        );
-       connect_button dialog#disambiguationErrorsMoreErrors
-        (fun _ -> return () ; raise UseLibrary);
-       connect_button dialog#disambiguationErrorsCancelButton fail;
-       dialog#disambiguationErrors#show ();
-       GtkThread.main ()
-
+        let newtxt =
+         String.concat "\n"
+          ("" ::
+            List.map
+             (fun k,desc -> 
+               let alias =
+                match k with
+                | DisambiguateTypes.Id id ->
+                    GrafiteAst.Ident_alias (id, desc)
+                | DisambiguateTypes.Symbol (symb, i)-> 
+                    GrafiteAst.Symbol_alias (symb, i, desc)
+                | DisambiguateTypes.Num i ->
+                    GrafiteAst.Number_alias (i, desc)
+               in
+                GrafiteAstPp.pp_alias alias)
+             diff) ^ "\n"
+        in
+         source_buffer#insert
+          ~iter:
+            (source_buffer#get_iter_at_mark
+             (`NAME "beginning_of_statement")) newtxt
+    | `HELP (* HELP MEANS MORE *) ->
+        dialog#toplevel#destroy () ;
+        raise UseLibrary
+    | `DELETE_EVENT -> ()
+    | _ -> assert false) ;
+   dialog#toplevel#destroy ()
+  ) ()
 
 class gui () =
     (* creation order _is_ relevant for windows placement *)
@@ -461,6 +459,7 @@ class gui () =
         ~website:"http://matita.cs.unibo.it"
         ()
       in
+      ignore(about_dialog#event#connect#delete (fun _ -> true));
       ignore(about_dialog#connect#response (fun _ ->about_dialog#misc#hide ()));
       connect_menu_item main#contentsMenuItem (fun () ->
         if 0 = Sys.command "which gnome-help" then
@@ -932,7 +931,7 @@ class gui () =
              save_moo script#status;
              true
         | `NO -> true
-        | `CANCEL -> false
+        | `DELETE_EVENT -> false
       else 
        (save_moo script#status; true)
 
@@ -1136,6 +1135,7 @@ class interpModel =
 let interactive_string_choice 
   text prefix_len ?(title = "") ?(msg = "") () ~id locs uris 
 = 
+ GtkThread.sync (fun _ ->
  let dialog = new uriChoiceDialog () in
  dialog#uriEntryHBox#misc#hide ();
  dialog#uriChoiceSelectedButton#misc#hide ();
@@ -1144,7 +1144,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
@@ -1179,22 +1179,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;*)