X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaGtkMisc.ml;h=765ffb33e0d67ce7724a675fc6a1097f91abcf15;hb=a3994cfd56d213d6c78bcd654cbcceeb609f9d94;hp=2022704309e77c21f732386a67606c5b0b0b3247;hpb=82b7eb102431915258b4886465f0bdc3305b3ae1;p=helm.git

diff --git a/matita/matita/matitaGtkMisc.ml b/matita/matita/matitaGtkMisc.ml
index 202270430..765ffb33e 100644
--- a/matita/matita/matitaGtkMisc.ml
+++ b/matita/matita/matitaGtkMisc.ml
@@ -247,8 +247,6 @@ class recordModel (tree_view:GTree.view) =
 class type gui =
   object
     method newUriDialog:          unit -> MatitaGeneratedGui.uriChoiceDialog
-    method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog
-    method newEmptyDialog:        unit -> MatitaGeneratedGui.emptyDialog
   end
 
 let popup_message 
@@ -343,50 +341,6 @@ let report_error ~title ~message ?parent () =
   | PopupClosed -> ()
 
 
-let ask_text ~(gui:#gui) ?(title = "") ?(message = "") ?(multiline = false)
-  ?default ()
-=
-  let dialog = gui#newEmptyDialog () in
-  dialog#emptyDialog#set_title title;
-  dialog#emptyDialogLabel#set_label message;
-  let result = ref None in
-  let return r =
-    result := r;
-    dialog#emptyDialog#destroy ();
-    GMain.Main.quit ()
-  in
-  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#emptyDialogVBox#add ()
-    in
-    let view = GText.view ~wrap_mode:`CHAR ~packing:win#add () in
-    let buffer = view#buffer in
-    (match default with
-    | None -> ()
-    | Some text ->
-        buffer#set_text text;
-        buffer#select_range buffer#start_iter buffer#end_iter);
-    view#misc#grab_focus ();
-    connect_button dialog#emptyDialogOkButton (fun _ ->
-      return (Some (buffer#get_text ())))
-  end else begin (* monoline input required: use a TextEntry widget *)
-    let entry = GEdit.entry ~packing:dialog#emptyDialogVBox#add () in
-    (match default with
-    | None -> ()
-    | Some text ->
-        entry#set_text text;
-        entry#select_region ~start:0 ~stop:max_int);
-    entry#misc#grab_focus ();
-    connect_button dialog#emptyDialogOkButton (fun _ ->
-      return (Some entry#text))
-  end;
-  connect_button dialog#emptyDialogCancelButton (fun _ ->return None);
-  dialog#emptyDialog#show ();
-  GtkThread.main ();
-  (match !result with None -> raise MatitaTypes.Cancel | Some r -> r)
-
 let utf8_parsed_text s floc = 
   let start, stop = HExtlib.loc_of_floc floc in
   let start_bytes = Glib.Utf8.offset_to_pos s ~pos:0 ~off:start in