added extra "id" parameter for input_or_locate_uri callback

[helm.git] / helm / gTopLevel / gTopLevel.ml

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 988eb7e143e9a86ba563095a7dac0f4294976904..0d0b7c4d171afe54dd25b143cbce86194ca8965c 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -196,9 +196,9 @@ let check_window uris =
 
 exception NoChoice;;
 
-let
- interactive_user_uri_choice ~(selection_mode:[`MULTIPLE|`SINGLE]) ?(ok="Ok")
-  ?(enable_button_for_non_vars=false) ~title ~msg uris
+let interactive_user_uri_choice
+ ~(selection_mode:[ `SINGLE | `MULTIPLE ])
+ ?(ok="Ok") ?(enable_button_for_non_vars=false) ~title ~msg uris
 =
  let only_constant_choices =
    lazy
@@ -1055,7 +1055,7 @@ module DisambiguateCallbacks =
     interactive_user_uri_choice ~selection_mode ?ok
      ?enable_button_for_non_vars ~title ~msg
   let interactive_interpretation_choice = interactive_interpretation_choice
-  let input_or_locate_uri = input_or_locate_uri
+  let input_or_locate_uri ~title ?id = input_or_locate_uri ~title
  end
 ;;