added choose_uri method to console, used by the interpreter to implement the

[helm.git] / helm / matita / matitaTypes.ml

diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index a9e74bf5fdbf1e0bef21d76681dc61481454a85d..73a5da1a1c3bc863df34b0516c9724e0b709c09e 100644 (file)
--- a/helm/matita/matitaTypes.ml
+++ b/helm/matita/matitaTypes.ml
@@ -75,6 +75,8 @@ class type console =
     method echo_error     : string -> unit
     method clear          : unit -> unit
     method wrap_exn       : 'a. (unit -> 'a) -> 'a option
+    method choose_uri     : string list -> string
+    method show : ?msg:string -> unit -> unit
   end
 
 type choose_uris_callback =