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

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

diff --git a/helm/matita/matitac.ml b/helm/matita/matitac.ml
index 2ae1c8d6846b635d1dca96a10121bb4ef0224969..533bbc6a3d46df166290596df4da29ed2a745ae4 100644 (file)
--- a/helm/matita/matitac.ml
+++ b/helm/matita/matitac.ml
@@ -46,6 +46,8 @@ class tty_console =
       with exn ->
         self#echo_error (explain exn);
         None
+    method show ?(msg = "") () = assert false; ()
+    method choose_uri (uris: string list): string = assert false
   end
 
 (** {2 Initialization} *)