new tacticals

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

diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml
index 686f54399327801a5193dd0c42dfa7df18fef898..0ad36dfee8f5e04fd3d255b42e6dc8ee0adaadb8 100644 (file)
--- a/helm/matita/matitaGtkMisc.ml
+++ b/helm/matita/matitaGtkMisc.ml
@@ -307,7 +307,9 @@ let report_error ~title ~message ?parent () =
   | PopupClosed -> ()
 
 
-let ask_text ~(gui:#gui) ?(title = "") ?(msg = "") ?(multiline = false) () =
+let ask_text ~(gui:#gui) ?(title = "") ?(msg = "") ?(multiline = false)
+  ?default ()
+=
   let dialog = gui#newEmptyDialog () in
   dialog#emptyDialog#set_title title;
   dialog#emptyDialogLabel#set_label msg;
@@ -324,11 +326,22 @@ let ask_text ~(gui:#gui) ?(title = "") ?(msg = "") ?(multiline = false) () =
         ~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 (view#buffer#get_text ())))
+      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))