X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.mli;h=674f3702cec56241bfd6d10af607e2f0ef394dc6;hb=fd372e069bbcaa96dc5b2eef04f341b28850d726;hp=cb2cbeb0c00ef46775cb549b4d54b8d62d7d538c;hpb=de4483296d06aac3df4da10d5401b1f97c4350ab;p=helm.git diff --git a/helm/matita/matitaGui.mli b/helm/matita/matitaGui.mli index cb2cbeb0c..674f3702c 100644 --- a/helm/matita/matitaGui.mli +++ b/helm/matita/matitaGui.mli @@ -34,6 +34,12 @@ object method log_callback: MatitaLog.log_callback end +class type browserWin = +object + inherit MatitaGeneratedGui.browserWin + method browserUri: GEdit.combo_box_entry +end + (** @param fname name of the Glade file describing the GUI *) class type gui = object @@ -53,7 +59,7 @@ object * methods below create a new window on each invocation. You should * remember to destroy windows after use *) - method newBrowserWin: unit -> MatitaGeneratedGui.browserWin + method newBrowserWin: unit -> browserWin method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog method newInterpDialog: unit -> MatitaGeneratedGui.interpChoiceDialog method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog @@ -88,6 +94,7 @@ val interactive_uri_choice: ?selection_mode:([`SINGLE|`MULTIPLE]) -> ?title:string -> ?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