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
+