several dialog boxes no longer used removed

they were dead code in current Matita
I only left the AutoWin and the ones used

diff --git a/matita/matita/matita.ui b/matita/matita/matita.ui
index 4cbc20a0fdcea8bbca844e0eaedcf861ad5926af..731419c1c8c6c4c3aa1257f85f39c29d1ef84dca 100644 (file)
--- a/matita/matita/matita.ui
+++ b/matita/matita/matita.ui
@@ -743,81 +743,6 @@
       </object>
     </child>
   </object>
-  <object class="GtkDialog" id="ConfirmationDialog">
-    <property name="can_focus">False</property>
-    <property name="title" translatable="yes">DUMMY</property>
-    <property name="resizable">False</property>
-    <property name="modal">True</property>
-    <property name="window_position">center</property>
-    <property name="type_hint">dialog</property>
-    <child internal-child="vbox">
-      <object class="GtkBox" id="dialog-vbox1">
-        <property name="visible">True</property>
-        <property name="can_focus">False</property>
-        <property name="orientation">vertical</property>
-        <child internal-child="action_area">
-          <object class="GtkButtonBox" id="dialog-action_area1">
-            <property name="visible">True</property>
-            <property name="can_focus">False</property>
-            <property name="layout_style">end</property>
-            <child>
-              <object class="GtkButton" id="ConfirmationDialogCancelButton">
-                <property name="label">gtk-cancel</property>
-                <property name="visible">True</property>
-                <property name="can_focus">True</property>
-                <property name="can_default">True</property>
-                <property name="receives_default">False</property>
-                <property name="use_stock">True</property>
-              </object>
-              <packing>
-                <property name="expand">False</property>
-                <property name="fill">False</property>
-                <property name="position">0</property>
-              </packing>
-            </child>
-            <child>
-              <object class="GtkButton" id="ConfirmationDialogOkButton">
-                <property name="label">gtk-ok</property>
-                <property name="visible">True</property>
-                <property name="can_focus">True</property>
-                <property name="can_default">True</property>
-                <property name="receives_default">False</property>
-                <property name="use_stock">True</property>
-              </object>
-              <packing>
-                <property name="expand">False</property>
-                <property name="fill">False</property>
-                <property name="position">1</property>
-              </packing>
-            </child>
-          </object>
-          <packing>
-            <property name="expand">False</property>
-            <property name="fill">False</property>
-            <property name="pack_type">end</property>
-            <property name="position">0</property>
-          </packing>
-        </child>
-        <child>
-          <object class="GtkLabel" id="ConfirmationDialogLabel">
-            <property name="visible">True</property>
-            <property name="can_focus">False</property>
-            <property name="label" translatable="yes">DUMMY</property>
-            <property name="justify">center</property>
-          </object>
-          <packing>
-            <property name="expand">False</property>
-            <property name="fill">False</property>
-            <property name="position">2</property>
-          </packing>
-        </child>
-      </object>
-    </child>
-    <action-widgets>
-      <action-widget response="-6">ConfirmationDialogCancelButton</action-widget>
-      <action-widget response="-5">ConfirmationDialogOkButton</action-widget>
-    </action-widgets>
-  </object>
   <object class="GtkDialog" id="DisambiguationErrors">
     <property name="width_request">450</property>
     <property name="height_request">400</property>
@@ -997,78 +922,6 @@
       <action-widget response="-5">disambiguationErrorsOkButton</action-widget>
     </action-widgets>
   </object>
-  <object class="GtkDialog" id="EmptyDialog">
-    <property name="visible">True</property>
-    <property name="can_focus">False</property>
-    <property name="title" translatable="yes">DUMMY</property>
-    <property name="type_hint">dialog</property>
-    <child internal-child="vbox">
-      <object class="GtkBox" id="EmptyDialogVBox">
-        <property name="visible">True</property>
-        <property name="can_focus">False</property>
-        <property name="orientation">vertical</property>
-        <child internal-child="action_area">
-          <object class="GtkButtonBox" id="dialog-action_area5">
-            <property name="visible">True</property>
-            <property name="can_focus">False</property>
-            <property name="layout_style">end</property>
-            <child>
-              <object class="GtkButton" id="EmptyDialogCancelButton">
-                <property name="label">gtk-cancel</property>
-                <property name="visible">True</property>
-                <property name="can_focus">True</property>
-                <property name="can_default">True</property>
-                <property name="receives_default">False</property>
-                <property name="use_stock">True</property>
-              </object>
-              <packing>
-                <property name="expand">False</property>
-                <property name="fill">False</property>
-                <property name="position">0</property>
-              </packing>
-            </child>
-            <child>
-              <object class="GtkButton" id="EmptyDialogOkButton">
-                <property name="label">gtk-ok</property>
-                <property name="visible">True</property>
-                <property name="can_focus">True</property>
-                <property name="can_default">True</property>
-                <property name="receives_default">False</property>
-                <property name="use_stock">True</property>
-              </object>
-              <packing>
-                <property name="expand">False</property>
-                <property name="fill">False</property>
-                <property name="position">1</property>
-              </packing>
-            </child>
-          </object>
-          <packing>
-            <property name="expand">False</property>
-            <property name="fill">False</property>
-            <property name="pack_type">end</property>
-            <property name="position">0</property>
-          </packing>
-        </child>
-        <child>
-          <object class="GtkLabel" id="EmptyDialogLabel">
-            <property name="visible">True</property>
-            <property name="can_focus">False</property>
-            <property name="label" translatable="yes">DUMMY</property>
-          </object>
-          <packing>
-            <property name="expand">False</property>
-            <property name="fill">False</property>
-            <property name="position">2</property>
-          </packing>
-        </child>
-      </object>
-    </child>
-    <action-widgets>
-      <action-widget response="-6">EmptyDialogCancelButton</action-widget>
-      <action-widget response="-5">EmptyDialogOkButton</action-widget>
-    </action-widgets>
-  </object>
   <object class="GtkWindow" id="FindReplWin">
     <property name="can_focus">False</property>
     <property name="border_width">5</property>
@@ -2591,95 +2444,6 @@
       </object>
     </child>
   </object>
-  <object class="GtkDialog" id="TextDialog">
-    <property name="can_focus">False</property>
-    <property name="title" translatable="yes">DUMMY</property>
-    <property name="type_hint">dialog</property>
-    <child internal-child="vbox">
-      <object class="GtkBox" id="vbox5">
-        <property name="visible">True</property>
-        <property name="can_focus">False</property>
-        <property name="orientation">vertical</property>
-        <child internal-child="action_area">
-          <object class="GtkButtonBox" id="hbuttonbox1">
-            <property name="visible">True</property>
-            <property name="can_focus">False</property>
-            <property name="layout_style">end</property>
-            <child>
-              <object class="GtkButton" id="TextDialogCancelButton">
-                <property name="label">gtk-cancel</property>
-                <property name="visible">True</property>
-                <property name="can_focus">True</property>
-                <property name="can_default">True</property>
-                <property name="receives_default">False</property>
-                <property name="use_stock">True</property>
-              </object>
-              <packing>
-                <property name="expand">False</property>
-                <property name="fill">False</property>
-                <property name="position">0</property>
-              </packing>
-            </child>
-            <child>
-              <object class="GtkButton" id="TextDialogOkButton">
-                <property name="label">gtk-ok</property>
-                <property name="visible">True</property>
-                <property name="can_focus">True</property>
-                <property name="can_default">True</property>
-                <property name="receives_default">False</property>
-                <property name="use_stock">True</property>
-              </object>
-              <packing>
-                <property name="expand">False</property>
-                <property name="fill">False</property>
-                <property name="position">1</property>
-              </packing>
-            </child>
-          </object>
-          <packing>
-            <property name="expand">False</property>
-            <property name="fill">False</property>
-            <property name="pack_type">end</property>
-            <property name="position">0</property>
-          </packing>
-        </child>
-        <child>
-          <object class="GtkLabel" id="TextDialogLabel">
-            <property name="visible">True</property>
-            <property name="can_focus">False</property>
-            <property name="label" translatable="yes">DUMMY</property>
-          </object>
-          <packing>
-            <property name="expand">False</property>
-            <property name="fill">False</property>
-            <property name="position">2</property>
-          </packing>
-        </child>
-        <child>
-          <object class="GtkScrolledWindow" id="scrolledwindow2">
-            <property name="visible">True</property>
-            <property name="can_focus">True</property>
-            <property name="shadow_type">in</property>
-            <child>
-              <object class="GtkTextView" id="TextDialogTextView">
-                <property name="visible">True</property>
-                <property name="can_focus">True</property>
-              </object>
-            </child>
-          </object>
-          <packing>
-            <property name="expand">False</property>
-            <property name="fill">True</property>
-            <property name="position">3</property>
-          </packing>
-        </child>
-      </object>
-    </child>
-    <action-widgets>
-      <action-widget response="-6">TextDialogCancelButton</action-widget>
-      <action-widget response="-5">TextDialogOkButton</action-widget>
-    </action-widgets>
-  </object>
   <object class="GtkDialog" id="UriChoiceDialog">
     <property name="height_request">280</property>
     <property name="can_focus">False</property>

diff --git a/matita/matita/matitaGtkMisc.ml b/matita/matita/matitaGtkMisc.ml
index 2022704309e77c21f732386a67606c5b0b0b3247..765ffb33e0d67ce7724a675fc6a1097f91abcf15 100644 (file)
--- 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

diff --git a/matita/matita/matitaGtkMisc.mli b/matita/matita/matitaGtkMisc.mli
index cf4ce93a9d17e836119410bb93dc99466c0369b0..627909cd456e4e1b5969a8171e60d262469b0fc5 100644 (file)
--- a/matita/matita/matitaGtkMisc.mli
+++ b/matita/matita/matitaGtkMisc.mli
@@ -111,8 +111,6 @@ class taggedStringListModel:
 class type gui =
   object  (* minimal gui object requirements *)
     method newUriDialog:          unit -> MatitaGeneratedGui.uriChoiceDialog
-    method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog
-    method newEmptyDialog:        unit -> MatitaGeneratedGui.emptyDialog
   end
 
   (** {3 Dialogs}
@@ -127,15 +125,6 @@ val ask_confirmation:
   unit ->
     [`YES | `NO | `CANCEL]
 
-  (** @param multiline (default: false) if true a TextView widget will be used
-  * for prompting the user otherwise a TextEntry widget will be
-  * @return the string given by the user *)
-val ask_text:
-  gui:#gui ->
-  ?title:string -> ?message:string ->
-  ?multiline:bool -> ?default:string -> unit ->
-    string
-
 val report_error:
   title:string -> message:string -> 
   ?parent:#GWindow.window_skel ->