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

diff --git a/helm/matita/matitaConsole.mli b/helm/matita/matitaConsole.mli
index 950776135..a8e272e22 100644
--- a/helm/matita/matitaConsole.mli
+++ b/helm/matita/matitaConsole.mli
@@ -26,14 +26,23 @@
   (** @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
@@ -42,9 +51,14 @@ class console:
     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.
+      * @return true if no exception has been raised, false otherwise *)
+    method wrap_exn       : (unit -> unit) -> bool
   end
 
   (** @param prompt user prompt (default "# ")
@@ -55,8 +69,9 @@ class console:
 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 ->