snapshot

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

diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml
index e24bf27c1ffae831247b0b42efb630e71a69aba4..2ff018a525586b973b20e2498272a1703472950a 100644 (file)
--- a/helm/matita/matitaGtkMisc.ml
+++ b/helm/matita/matitaGtkMisc.ml
@@ -86,13 +86,13 @@ class type gui =
   object
     method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog
     method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog
-    method newTextDialog: unit -> MatitaGeneratedGui.textDialog
+    method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog
   end
 
 exception Cancel
 
 let interactive_user_uri_choice
-  ~(gui:#gui) ~(selection_mode:Gtk.Tags.selection_mode) ?(title = "")
+  ~(gui:#gui) ~(selection_mode:[`SINGLE|`MULTIPLE]) ?(title = "")
   ?(msg = "") ?(nonvars_button=false) uris
 =
   let nonvars_uris = lazy (List.filter (non is_var_uri) uris) in
@@ -102,7 +102,8 @@ let interactive_user_uri_choice
     Lazy.force nonvars_uris
   else begin
     let dialog = gui#newUriDialog () in
-    dialog#uriChoiceTreeView#selection#set_mode selection_mode;
+    dialog#uriChoiceTreeView#selection#set_mode
+      (selection_mode :> Gtk.Tags.selection_mode);
     let model = new stringListModel dialog#uriChoiceTreeView in
     let choices = ref None in
     let nonvars = ref false in
@@ -157,31 +158,33 @@ let ask_confirmation ~(gui:#gui) ?(title = "") ?(msg = "") () =
   (match !result with None -> assert false | Some r -> r)
 
 let ask_text ~(gui:#gui) ?(title = "") ?(msg = "") ?(multiline = false) () =
-  let dialog = gui#newTextDialog () in
-  dialog#textDialog#set_title title;
-  dialog#textDialogLabel#set_label msg;
+  let dialog = gui#newEmptyDialog () in
+  dialog#emptyDialog#set_title title;
+  dialog#emptyDialogLabel#set_label msg;
   let result = ref None in
   let return r =
     result := r;
-    dialog#textDialog#destroy ();
+    dialog#emptyDialog#destroy ();
     GMain.Main.quit ()
   in
-  ignore (dialog#textDialog#event#connect#delete (fun _ -> true));
+  ignore (dialog#emptyDialog#event#connect#delete (fun _ -> true));
   if multiline then begin (* multiline input required: use a TextView widget *)
     let win =
       GBin.scrolled_window ~width:400 ~height:150 ~hpolicy:`NEVER
-        ~vpolicy:`ALWAYS ~packing:dialog#textDialogVBox#add ()
+        ~vpolicy:`ALWAYS ~packing:dialog#emptyDialogVBox#add ()
     in
     let view = GText.view ~wrap_mode:`CHAR ~packing:win#add () in
-    ignore (dialog#textDialogOkButton#connect#clicked (fun _ ->
+    view#misc#grab_focus ();
+    ignore (dialog#emptyDialogOkButton#connect#clicked (fun _ ->
       return (Some (view#buffer#get_text ()))))
   end else begin (* monoline input required: use a TextEntry widget *)
-    let entry = GEdit.entry ~packing:dialog#textDialogVBox#add () in
-    ignore (dialog#textDialogOkButton#connect#clicked (fun _ ->
+    let entry = GEdit.entry ~packing:dialog#emptyDialogVBox#add () in
+    entry#misc#grab_focus ();
+    ignore (dialog#emptyDialogOkButton#connect#clicked (fun _ ->
       return (Some entry#text)))
   end;
-  ignore (dialog#textDialogCancelButton#connect#clicked (fun _ -> return None));
-  dialog#textDialog#show ();
+  ignore (dialog#emptyDialogCancelButton#connect#clicked (fun _ ->return None));
+  dialog#emptyDialog#show ();
   GtkThread.main ();
   (match !result with None -> raise Cancel | Some r -> r)