* http://helm.cs.unibo.it/
*)
-class console: ?prompt:string -> Gtk.text_view Gtk.obj ->
+ (** @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 ->
object
inherit GText.view
- method read_phrase : unit -> string
+ method echo_prompt : unit -> unit
+ method echo_message : string -> unit
+ method echo_error : string -> unit
- method echo_prompt : unit -> unit
- 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
+
+ (** override previous callback definition *)
+ method set_callback : (string -> unit) -> unit
+
+ method ignore_insert_text_signal: bool -> unit
end
+ (** @param prompt user prompt (default "# ")
+ * @param phrase_sep phrase separator (default ".")
+ * @param callback callback invoked upon reading of a phrase. Callback
+ * may be invoked more than once if multiple phrases have been inserted before
+ * hitting return (default: do nothing) *)
val console :
?prompt:string ->
+ ?phrase_sep:string ->
+ ?callback:(string -> unit) ->
+ ?evbox:GBin.event_box ->
+
?buffer:GText.buffer ->
?editable:bool ->
?cursor_visible:bool ->