snapshot

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

diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml
index a87700941a12677fd8b2d311d1b886979683660b..80f5676cd7665ca66c0c59aaa5230d66934b9f64 100644 (file)
--- a/helm/matita/matitaGtkMisc.ml
+++ b/helm/matita/matitaGtkMisc.ml
@@ -82,16 +82,17 @@ let is_var_uri s =
 
 let non p x = not (p x)
 
-exception No_choice
-
 class type gui =
-  object method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog end
+  object
+    method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog
+    method newConfirmationDialog :
+      title:string -> msg:string -> unit ->
+        MatitaGeneratedGui.confirmationDialog
+  end
 
 let interactive_user_uri_choice
-(*   ~(gui: <newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog>) *)
-  ~(gui:#gui)
-  ~(selection_mode:Gtk.Tags.selection_mode) ~title ~msg ?(nonvars_button=false)
-  uris
+  ~(gui:#gui) ~(selection_mode:Gtk.Tags.selection_mode) ?(title = "")
+  ?(msg = "") ?(nonvars_button=false) uris
 =
   let nonvars_uris = lazy (List.filter (non is_var_uri) uris) in
   if (selection_mode <> `SINGLE) &&
@@ -99,33 +100,56 @@ let interactive_user_uri_choice
   then
     Lazy.force nonvars_uris
   else begin
-    let win = gui#newUriDialog () in
-    win#uriChoiceTreeView#selection#set_mode selection_mode;
-    let model = new stringListModel win#uriChoiceTreeView in
+    let dialog = gui#newUriDialog () in
+    dialog#uriChoiceTreeView#selection#set_mode selection_mode;
+    let model = new stringListModel dialog#uriChoiceTreeView in
     let choices = ref None in
     let nonvars = ref false in
-    win#uriChoiceDialog#set_title title;
-    win#uriChoiceLabel#set_text msg;
+    dialog#uriChoiceDialog#set_title title;
+    dialog#uriChoiceLabel#set_text msg;
     List.iter model#easy_append uris;
-    win#uriChoiceConstantsButton#misc#set_sensitive nonvars_button;
+    dialog#uriChoiceConstantsButton#misc#set_sensitive nonvars_button;
     let return v =
       choices := v;
-      win#uriChoiceDialog#destroy ();
+      dialog#uriChoiceDialog#destroy ();
       GMain.Main.quit ()
     in
-    ignore (win#uriChoiceConstantsButton#connect#clicked (fun _ ->
+    ignore (dialog#uriChoiceConstantsButton#connect#clicked (fun _ ->
       return (Some (Lazy.force nonvars_uris))));
-    ignore (win#uriChoiceAutoButton#connect#clicked (fun _ ->
+    ignore (dialog#uriChoiceAutoButton#connect#clicked (fun _ ->
       Helm_registry.set_bool "matita.auto_disambiguation" true;
       return (Some (Lazy.force nonvars_uris))));
-    ignore (win#uriChoiceSelectedButton#connect#clicked (fun _ ->
+    ignore (dialog#uriChoiceSelectedButton#connect#clicked (fun _ ->
       match model#easy_selection () with
       | [] -> ()
       | uris -> return (Some uris)));
-    ignore (win#uriChoiceAbortButton#connect#clicked (fun _ -> return None));
-    ignore (win#uriChoiceDialog#event#connect#delete (fun _ -> true));
-    win#uriChoiceDialog#show ();
+    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 No_choice | Some uris -> uris)
+    (match !choices with 
+    | None -> raise MatitaTypes.No_choice
+    | Some uris -> uris)
   end
 
+let interactive_interp_choice ~(gui:#gui) choices =
+  (* TODO Zack implement interactive_interp_choice *)
+  MatitaTypes.warning
+    "'interactive_interp_choice' not implemented: returning 1st interpretation";
+  [0]
+
+let ask_confirmation ~(gui:#gui) ?(title = "") ?(msg = "") () =
+  let dialog = gui#newConfirmationDialog ~title ~msg () in
+  let result = ref None in
+  let return r _ =
+    result := Some r;
+    dialog#confirmationDialog#destroy ();
+    GMain.Main.quit ()
+  in
+  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)
+