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

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

diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli
index 538b4b3243406b36039db5b9e7b46e227b0a738e..1db5bb0de04ea2efb8454458d3da9b73d00f8478 100644 (file)
--- a/helm/matita/matitaTypes.mli
+++ b/helm/matita/matitaTypes.mli
@@ -72,6 +72,8 @@ class type console =
     method echo_error : string -> unit
     method echo_message : string -> unit
     method wrap_exn : 'a. (unit -> 'a) -> 'a option
+    method choose_uri : string list -> string
+    method show : ?msg:string -> unit -> unit
   end
 
 class type disambiguator =