From: Luca Padovani Date: Wed, 29 Oct 2003 09:17:30 +0000 (+0000) Subject: * variant types changed for selection mode X-Git-Tag: V_0_2_2~44 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4019f7f93ffc05e4ca98bcaafc8a681adff040b6;p=helm.git * variant types changed for selection mode --- diff --git a/helm/gTopLevel/disambiguate.ml b/helm/gTopLevel/disambiguate.ml index ce41208dd..974e0b49e 100644 --- a/helm/gTopLevel/disambiguate.ml +++ b/helm/gTopLevel/disambiguate.ml @@ -46,7 +46,7 @@ module type Callbacks = val output_html : string -> unit val interactive_user_uri_choice : - selection_mode:[`SINGLE | `EXTENDED] -> + selection_mode:[`SINGLE | `MULTIPLE] -> ?ok:string -> ?enable_button_for_non_vars:bool -> title:string -> msg:string -> id:string -> string list -> string list @@ -85,7 +85,7 @@ module Make(C:Callbacks) = | [uri] -> [uri] | _ -> C.interactive_user_uri_choice - ~selection_mode:`EXTENDED + ~selection_mode:`MULTIPLE ~ok:"Try every selection." ~enable_button_for_non_vars:true ~title:"Ambiguous input." diff --git a/helm/gTopLevel/disambiguate.mli b/helm/gTopLevel/disambiguate.mli index 9fdfb8993..0114ce27f 100644 --- a/helm/gTopLevel/disambiguate.mli +++ b/helm/gTopLevel/disambiguate.mli @@ -46,7 +46,7 @@ module type Callbacks = val output_html : string -> unit val interactive_user_uri_choice : - selection_mode:[`SINGLE | `EXTENDED] -> + selection_mode:[`SINGLE | `MULTIPLE] -> ?ok:string -> ?enable_button_for_non_vars:bool -> title:string -> msg:string -> id:string -> string list -> string list