X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGtkMisc.ml;h=a87700941a12677fd8b2d311d1b886979683660b;hb=b5d69130dd83587b5fb9cbb39251aaa8df8c456e;hp=fc4fecc8f14154080105e78e991faf65b00809ac;hpb=c5d4ad1c98c1434b95a8a9b1c8697dd36cf39623;p=helm.git

diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml
index fc4fecc8f..a87700941 100644
--- a/helm/matita/matitaGtkMisc.ml
+++ b/helm/matita/matitaGtkMisc.ml
@@ -75,3 +75,57 @@ 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)
+
+exception No_choice
+
+class type gui =
+  object method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog 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
+=
+  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 win = gui#newUriDialog () in
+    win#uriChoiceTreeView#selection#set_mode selection_mode;
+    let model = new stringListModel win#uriChoiceTreeView in
+    let choices = ref None in
+    let nonvars = ref false in
+    win#uriChoiceDialog#set_title title;
+    win#uriChoiceLabel#set_text msg;
+    List.iter model#easy_append uris;
+    win#uriChoiceConstantsButton#misc#set_sensitive nonvars_button;
+    let return v =
+      choices := v;
+      win#uriChoiceDialog#destroy ();
+      GMain.Main.quit ()
+    in
+    ignore (win#uriChoiceConstantsButton#connect#clicked (fun _ ->
+      return (Some (Lazy.force nonvars_uris))));
+    ignore (win#uriChoiceAutoButton#connect#clicked (fun _ ->
+      Helm_registry.set_bool "matita.auto_disambiguation" true;
+      return (Some (Lazy.force nonvars_uris))));
+    ignore (win#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 ();
+    GtkThread.main ();
+    (match !choices with None -> raise No_choice | Some uris -> uris)
+  end
+