(** @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) ->
- ?evbox:GBin.event_box -> Gtk.text_view Gtk.obj ->
+ ?prompt:string -> ?phrase_sep:string -> ?callback:(string -> bool) ->
+ ?evbox:GBin.event_box -> paned:GPack.paned -> Gtk.text_view Gtk.obj ->
object
inherit GText.view
method echo_prompt : unit -> unit
method echo_message : string -> unit
method echo_error : string -> unit
+ method clear : unit -> unit
+
+ (* console visibility handling inside VPaned *)
+
+ (** @param msg if given, show the console with a prefeed input, cursor
+ * just after it; defaults to the empty string *)
+ method show : ?msg:string -> unit -> unit
+ method hide : unit -> unit
+(* method toggle : unit -> unit *)
method prompt : string
method set_prompt : string -> unit
method set_phrase_sep : string -> unit
(** override previous callback definition *)
- method set_callback : (string -> unit) -> unit
+ method set_callback : (string -> bool) -> unit
method ignore_insert_text_signal: bool -> unit
+
+ (** execute a unit -> unit function, if it raises exceptions shows them as
+ * errors in the console *)
+ method wrap_exn : (unit -> unit) -> unit
end
(** @param prompt user prompt (default "# ")
val console :
?prompt:string ->
?phrase_sep:string ->
- ?callback:(string -> unit) ->
+ ?callback:(string -> bool) ->
?evbox:GBin.event_box ->
+ paned:GPack.paned ->
?buffer:GText.buffer ->
?editable:bool ->