snapshot (notably: first working version of the console)

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

diff --git a/helm/matita/matitaConsole.mli b/helm/matita/matitaConsole.mli
index ee7b8d4fb351445e7552073271e0ccef006f0c5e..2cbd1ffe33d33c5c6f97afbe20ed7a7b815721fe 100644 (file)
--- a/helm/matita/matitaConsole.mli
+++ b/helm/matita/matitaConsole.mli
@@ -38,6 +38,8 @@ class console:
 
       (** override previous callback definition *)
     method set_callback   : (string -> unit) -> unit
+
+    method ignore_insert_text_signal: bool -> unit
   end
 
   (** @param prompt user prompt (default "# ")