X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaConsole.mli;h=d0d1a53d3febad4bbc31afd0451a34383666460b;hb=7e9904185ceff75884783dbf0bad506b8521b857;hp=a8e272e227d0826cc4db167a344e9ee4abc0fbbb;hpb=e35ec00b1be70e4b064b74a49735b37b5e719e5b;p=helm.git

diff --git a/helm/matita/matitaConsole.mli b/helm/matita/matitaConsole.mli
index a8e272e22..d0d1a53d3 100644
--- a/helm/matita/matitaConsole.mli
+++ b/helm/matita/matitaConsole.mli
@@ -23,10 +23,12 @@
  * http://helm.cs.unibo.it/
  *)
 
+type callback = string -> MatitaTypes.command_outcome
+
   (** @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 -> bool) ->
+  ?prompt:string -> ?phrase_sep:string -> ?callback:callback ->
   ?evbox:GBin.event_box -> paned:GPack.paned -> Gtk.text_view Gtk.obj ->
   object
     inherit GText.view
@@ -51,14 +53,15 @@ class console:
     method set_phrase_sep : string -> unit
 
       (** override previous callback definition *)
-    method set_callback   : (string -> bool) -> unit
+    method set_callback   : callback -> unit
 
     method ignore_insert_text_signal: bool -> unit
 
-      (** execute a unit -> unit function, if it raises exceptions shows them as
+      (** execute a unit -> 'a 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
+      * @return Some of the returned value if the given function suceeds, None
+      * otherwise *)
+    method wrap_exn       : 'a. (unit -> 'a) -> 'a option
   end
 
   (** @param prompt user prompt (default "# ")
@@ -69,7 +72,7 @@ class console:
 val console :
   ?prompt:string ->
   ?phrase_sep:string ->
-  ?callback:(string -> bool) ->
+  ?callback:callback ->
   ?evbox:GBin.event_box ->
   paned:GPack.paned ->