X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=0d0b7c4d171afe54dd25b143cbce86194ca8965c;hb=eb8dc961c7f9dc2e76a1eb29e2fcf94304011566;hp=988eb7e143e9a86ba563095a7dac0f4294976904;hpb=947e7893dbb23fcaa998266ee8dd9a32b27d3b6e;p=helm.git

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 988eb7e14..0d0b7c4d1 100644
--- 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
 ;;