snapshot

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

diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml
index fc4fecc8f14154080105e78e991faf65b00809ac..80f5676cd7665ca66c0c59aaa5230d66934b9f64 100644 (file)
--- a/helm/matita/matitaGtkMisc.ml
+++ b/helm/matita/matitaGtkMisc.ml
@@ -75,3 +75,81 @@ class stringListModel (tree_view: GTree.view) =
 
   end
 
+let is_var_uri s =
+  try
+    String.sub s (String.length s - 4) 4 = ".var"
+  with Invalid_argument _ -> false
+
+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
+  end
+
+let interactive_user_uri_choice
+  ~(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) &&
+    (Helm_registry.get_bool "matita.auto_disambiguation")
+  then
+    Lazy.force nonvars_uris
+  else begin
+    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
+    dialog#uriChoiceDialog#set_title title;
+    dialog#uriChoiceLabel#set_text msg;
+    List.iter model#easy_append uris;
+    dialog#uriChoiceConstantsButton#misc#set_sensitive nonvars_button;
+    let return v =
+      choices := v;
+      dialog#uriChoiceDialog#destroy ();
+      GMain.Main.quit ()
+    in
+    ignore (dialog#uriChoiceConstantsButton#connect#clicked (fun _ ->
+      return (Some (Lazy.force nonvars_uris))));
+    ignore (dialog#uriChoiceAutoButton#connect#clicked (fun _ ->
+      Helm_registry.set_bool "matita.auto_disambiguation" true;
+      return (Some (Lazy.force nonvars_uris))));
+    ignore (dialog#uriChoiceSelectedButton#connect#clicked (fun _ ->
+      match model#easy_selection () with
+      | [] -> ()
+      | 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
+    | 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)
+