X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaConsole.mli;h=950776135426b6b1aa941f0c0aa05d9efebb0351;hb=a7ab0ef67114c3152920f03ae1d7bfaaf1fae290;hp=2cbd1ffe33d33c5c6f97afbe20ed7a7b815721fe;hpb=4cf419a2e770f4971be7b03b1d73e585d973dc1b;p=helm.git diff --git a/helm/matita/matitaConsole.mli b/helm/matita/matitaConsole.mli index 2cbd1ffe3..950776135 100644 --- a/helm/matita/matitaConsole.mli +++ b/helm/matita/matitaConsole.mli @@ -23,9 +23,11 @@ * http://helm.cs.unibo.it/ *) + (** @param evbox event box to which keyboard shortcuts are registered; no + * shortcut will be registered if evbox is not given *) class console: ?prompt:string -> ?phrase_sep:string -> ?callback:(string -> unit) -> - Gtk.text_view Gtk.obj -> + ?evbox:GBin.event_box -> Gtk.text_view Gtk.obj -> object inherit GText.view @@ -33,6 +35,9 @@ class console: method echo_message : string -> unit method echo_error : string -> unit + method prompt : string + method set_prompt : string -> unit + method phrase_sep : string method set_phrase_sep : string -> unit @@ -51,6 +56,7 @@ val console : ?prompt:string -> ?phrase_sep:string -> ?callback:(string -> unit) -> + ?evbox:GBin.event_box -> ?buffer:GText.buffer -> ?editable:bool ->