+(* this is a shit and should be changed :-{ *)
+let interactive_uri_choice
+ ?(selection_mode:[`SINGLE|`MULTIPLE] = `MULTIPLE) ?(title = "")
+ ?(msg = "") ?(nonvars_button = false) ?(hide_uri_entry=false)
+ ?(hide_try=false) ?(ok_label="_Auto") ?(ok_action:[`SELECT|`AUTO] = `AUTO)
+ ?copy_cb ()
+ ~id uris
+=
+ let gui = MatitaMisc.get_gui () in
+ if (selection_mode <> `SINGLE) &&
+ (Helm_registry.get_opt_default Helm_registry.get_bool ~default:true "matita.auto_disambiguation")
+ then
+ uris
+ else begin
+ let dialog = gui#newUriDialog () in
+ if hide_uri_entry then
+ dialog#uriEntryHBox#misc#hide ();
+ if hide_try then
+ begin
+ dialog#uriChoiceSelectedButton#misc#hide ();
+ dialog#uriChoiceConstantsButton#misc#hide ();
+ end;
+ dialog#okLabel#set_label ok_label;
+ dialog#uriChoiceTreeView#selection#set_mode
+ (selection_mode :> Gtk.Tags.selection_mode);
+ let model = new stringListModel dialog#uriChoiceTreeView in
+ let choices = ref None in
+ (match copy_cb with
+ | None -> ()
+ | Some cb ->
+ dialog#copyButton#misc#show ();
+ connect_button dialog#copyButton
+ (fun _ ->
+ match model#easy_selection () with
+ | [u] -> (cb u)
+ | _ -> ()));
+ dialog#uriChoiceDialog#set_title title;
+ dialog#uriChoiceLabel#set_text msg;
+ List.iter model#easy_append (List.map NReference.string_of_reference uris);
+ dialog#uriChoiceConstantsButton#misc#set_sensitive nonvars_button;
+ let return v =
+ choices := v;
+ dialog#uriChoiceDialog#destroy ();
+ GMain.Main.quit ()
+ in
+ ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true));
+ connect_button dialog#uriChoiceConstantsButton (fun _ ->
+ return (Some uris));
+ if ok_action = `AUTO then
+ connect_button dialog#uriChoiceAutoButton (fun _ ->
+ Helm_registry.set_bool "matita.auto_disambiguation" true;
+ return (Some uris))
+ else
+ connect_button dialog#uriChoiceAutoButton (fun _ ->
+ match model#easy_selection () with
+ | [] -> ()
+ | uris -> return (Some (List.map NReference.reference_of_string uris)));
+ connect_button dialog#uriChoiceSelectedButton (fun _ ->
+ match model#easy_selection () with
+ | [] -> ()
+ | uris -> return (Some (List.map NReference.reference_of_string uris)));
+ connect_button dialog#uriChoiceAbortButton (fun _ -> return None);
+ dialog#uriChoiceDialog#show ();
+ GtkThread.main ();
+ (match !choices with
+ | None -> raise MatitaTypes.Cancel
+ | Some uris -> uris)
+ end
+
+