X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaConsole.mli;h=950776135426b6b1aa941f0c0aa05d9efebb0351;hb=21758b512843088d19e81830d9fb121725c8a16e;hp=1bc5f7b9515d90dd4d5be88ca4b867d45ada5c66;hpb=481992ea591bf53cba758a96e7d42e9cdce7e129;p=helm.git

diff --git a/helm/matita/matitaConsole.mli b/helm/matita/matitaConsole.mli
index 1bc5f7b95..950776135 100644
--- a/helm/matita/matitaConsole.mli
+++ b/helm/matita/matitaConsole.mli
@@ -23,19 +23,41 @@
  * 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 ->