]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/matitaGtkMisc.mli
several dialog boxes no longer used removed
[helm.git] / matita / matita / matitaGtkMisc.mli
index cf4ce93a9d17e836119410bb93dc99466c0369b0..627909cd456e4e1b5969a8171e60d262469b0fc5 100644 (file)
@@ -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 ->