From: Claudio Sacerdoti Coen Date: Sat, 22 Dec 2018 00:19:30 +0000 (+0100) Subject: several dialog boxes no longer used removed X-Git-Tag: make_still_working~229^2~1^2~26 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=112c67fcdd49e3258a8644a5f299669741d9737d 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 4cbc20a0f..731419c1c 100644 --- a/matita/matita/matita.ui +++ b/matita/matita/matita.ui @@ -743,81 +743,6 @@ - - False - DUMMY - False - True - center - dialog - - - True - False - vertical - - - True - False - end - - - gtk-cancel - True - True - True - False - True - - - False - False - 0 - - - - - gtk-ok - True - True - True - False - True - - - False - False - 1 - - - - - False - False - end - 0 - - - - - True - False - DUMMY - center - - - False - False - 2 - - - - - - ConfirmationDialogCancelButton - ConfirmationDialogOkButton - - 450 400 @@ -997,78 +922,6 @@ disambiguationErrorsOkButton - - True - False - DUMMY - dialog - - - True - False - vertical - - - True - False - end - - - gtk-cancel - True - True - True - False - True - - - False - False - 0 - - - - - gtk-ok - True - True - True - False - True - - - False - False - 1 - - - - - False - False - end - 0 - - - - - True - False - DUMMY - - - False - False - 2 - - - - - - EmptyDialogCancelButton - EmptyDialogOkButton - - False 5 @@ -2591,95 +2444,6 @@ - - False - DUMMY - dialog - - - True - False - vertical - - - True - False - end - - - gtk-cancel - True - True - True - False - True - - - False - False - 0 - - - - - gtk-ok - True - True - True - False - True - - - False - False - 1 - - - - - False - False - end - 0 - - - - - True - False - DUMMY - - - False - False - 2 - - - - - True - True - in - - - True - True - - - - - False - True - 3 - - - - - - TextDialogCancelButton - TextDialogOkButton - - 280 False 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 diff --git a/matita/matita/matitaGtkMisc.mli b/matita/matita/matitaGtkMisc.mli index cf4ce93a9..627909cd4 100644 --- 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 ->