X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.mli;h=f517bbb9cb3c59415cc6e87933e353af687e3ec5;hb=6376b9d56df8c0151a4cd5f35f2646d9922b5858;hp=aabcba1e8805441cd1c6cdd5bd1327e9ae91a4d9;hpb=de9a83f286eee12117fb478ea2db18f7faebac9a;p=helm.git diff --git a/helm/matita/matitaGui.mli b/helm/matita/matitaGui.mli index aabcba1e8..f517bbb9c 100644 --- a/helm/matita/matitaGui.mli +++ b/helm/matita/matitaGui.mli @@ -69,6 +69,8 @@ object (** prompt the user for a (multiline) text entry *) method askText: ?title:string -> ?msg:string -> unit -> string option + method loadScript: string -> unit + end (** singleton instance of the gui *) @@ -84,7 +86,10 @@ val instance: unit -> gui * @raise MatitaTypes.Cancel *) val interactive_uri_choice: ?selection_mode:([`SINGLE|`MULTIPLE]) -> ?title:string -> - ?msg:string -> ?nonvars_button:bool -> unit -> + ?msg:string -> ?nonvars_button:bool -> + ?hide_uri_entry:bool -> ?hide_try:bool -> ?ok_label:string -> + ?ok_action:[`AUTO|`SELECT] -> + ?copy_cb:(string -> unit) -> unit -> MatitaDisambiguator.choose_uris_callback (** @raise MatitaTypes.Cancel *)