X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGtkMisc.ml;h=e24bf27c1ffae831247b0b42efb630e71a69aba4;hb=cc465115cdeea9819f43a5ad219b07c4f928c43a;hp=80f5676cd7665ca66c0c59aaa5230d66934b9f64;hpb=07dde6f87105c18b28fc784b7d596a5d242e1225;p=helm.git

diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml
index 80f5676cd..e24bf27c1 100644
--- a/helm/matita/matitaGtkMisc.ml
+++ b/helm/matita/matitaGtkMisc.ml
@@ -85,11 +85,12 @@ let non p x = not (p x)
 class type gui =
   object
     method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog
-    method newConfirmationDialog :
-      title:string -> msg:string -> unit ->
-        MatitaGeneratedGui.confirmationDialog
+    method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog
+    method newTextDialog: unit -> MatitaGeneratedGui.textDialog
   end
 
+exception Cancel
+
 let interactive_user_uri_choice
   ~(gui:#gui) ~(selection_mode:Gtk.Tags.selection_mode) ?(title = "")
   ?(msg = "") ?(nonvars_button=false) uris
@@ -114,6 +115,7 @@ let interactive_user_uri_choice
       dialog#uriChoiceDialog#destroy ();
       GMain.Main.quit ()
     in
+    ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true));
     ignore (dialog#uriChoiceConstantsButton#connect#clicked (fun _ ->
       return (Some (Lazy.force nonvars_uris))));
     ignore (dialog#uriChoiceAutoButton#connect#clicked (fun _ ->
@@ -124,11 +126,10 @@ let interactive_user_uri_choice
       | [] -> ()
       | uris -> return (Some uris)));
     ignore (dialog#uriChoiceAbortButton#connect#clicked (fun _ -> return None));
-    ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true));
     dialog#uriChoiceDialog#show ();
     GtkThread.main ();
     (match !choices with 
-    | None -> raise MatitaTypes.No_choice
+    | None -> raise Cancel
     | Some uris -> uris)
   end
 
@@ -139,17 +140,48 @@ let interactive_interp_choice ~(gui:#gui) choices =
   [0]
 
 let ask_confirmation ~(gui:#gui) ?(title = "") ?(msg = "") () =
-  let dialog = gui#newConfirmationDialog ~title ~msg () in
+  let dialog = gui#newConfirmationDialog () in
+  dialog#confirmationDialog#set_title title;
+  dialog#confirmationDialogLabel#set_label msg;
   let result = ref None in
   let return r _ =
     result := Some r;
     dialog#confirmationDialog#destroy ();
     GMain.Main.quit ()
   in
+  ignore (dialog#confirmationDialog#event#connect#delete (fun _ -> true));
   ignore (dialog#confirmationDialogOkButton#connect#clicked (return true));
   ignore (dialog#confirmationDialogCancelButton#connect#clicked (return false));
-  ignore (dialog#confirmationDialog#event#connect#delete (fun _ -> true));
   dialog#confirmationDialog#show ();
   GtkThread.main ();
   (match !result with None -> assert false | Some r -> r)
 
+let ask_text ~(gui:#gui) ?(title = "") ?(msg = "") ?(multiline = false) () =
+  let dialog = gui#newTextDialog () in
+  dialog#textDialog#set_title title;
+  dialog#textDialogLabel#set_label msg;
+  let result = ref None in
+  let return r =
+    result := r;
+    dialog#textDialog#destroy ();
+    GMain.Main.quit ()
+  in
+  ignore (dialog#textDialog#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#textDialogVBox#add ()
+    in
+    let view = GText.view ~wrap_mode:`CHAR ~packing:win#add () in
+    ignore (dialog#textDialogOkButton#connect#clicked (fun _ ->
+      return (Some (view#buffer#get_text ()))))
+  end else begin (* monoline input required: use a TextEntry widget *)
+    let entry = GEdit.entry ~packing:dialog#textDialogVBox#add () in
+    ignore (dialog#textDialogOkButton#connect#clicked (fun _ ->
+      return (Some entry#text)))
+  end;
+  ignore (dialog#textDialogCancelButton#connect#clicked (fun _ -> return None));
+  dialog#textDialog#show ();
+  GtkThread.main ();
+  (match !result with None -> raise Cancel | Some r -> r)
+