renamed Http_client to Http_user_agent to avoid clashes with Gerd's

[helm.git] / helm / matita / matitaConsole.mli

diff --git a/helm/matita/matitaConsole.mli b/helm/matita/matitaConsole.mli
index ee7b8d4fb351445e7552073271e0ccef006f0c5e..950776135426b6b1aa941f0c0aa05d9efebb0351 100644 (file)
--- 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,11 +35,16 @@ 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
 
       (** override previous callback definition *)
     method set_callback   : (string -> unit) -> unit
+
+    method ignore_insert_text_signal: bool -> unit
   end
 
   (** @param prompt user prompt (default "# ")
@@ -49,6 +56,7 @@ val console :
   ?prompt:string ->
   ?phrase_sep:string ->
   ?callback:(string -> unit) ->
+  ?evbox:GBin.event_box ->
 
   ?buffer:GText.buffer ->
   ?editable:bool ->