filled toolbar and implemented buttons behaviours

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

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 6b70a498f05e43bd9b93d6f09b13cd7661683e08..d50a2f31964d5fe50865e9c24e674abf0672488a 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -164,6 +164,26 @@ class gui file =
       GtkThread.main ();
       chosen_file
 
+    method askText ?(title = "") ?(msg = "") () =
+      let dialog = new textDialog () in
+      dialog#textDialog#set_title title;
+      dialog#textDialogLabel#set_label msg;
+      let text = ref None in
+      let return v =
+        text := v;
+        dialog#textDialog#destroy ();
+        GMain.Main.quit ()
+      in
+      ignore (dialog#textDialog#event#connect#delete (fun _ -> true));
+      ignore (dialog#textDialogCancelButton#connect#clicked (fun _ ->
+        return None));
+      ignore (dialog#textDialogOkButton#connect#clicked (fun _ ->
+        let text = dialog#textDialogTextView#buffer#get_text () in
+        return (Some text)));
+      dialog#textDialog#show ();
+      GtkThread.main ();
+      !text
+
   end
 
 let instance =