snapshot

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

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index f5d873d1997c7c9fd7961d395b8f8b28e896dbc7..017f3955512668b579b8834c2f7a938e359b4b38 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -97,10 +97,13 @@ class gui file =
       dialog#check_widgets ();
       dialog
 
-    method newConfirmationDialog ~title ~msg () =
+    method newConfirmationDialog () =
       let dialog = new confirmationDialog ~file () in
-      dialog#confirmationDialog#set_title title;
-      dialog#confirmationDialogLabel#set_label msg;
+      dialog#check_widgets ();
+      dialog
+
+    method newTextDialog () =
+      let dialog = new textDialog ~file () in
       dialog#check_widgets ();
       dialog