moved lockScript to MatitaScript module

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

diff --git a/helm/matita/matitaGui.mli b/helm/matita/matitaGui.mli
index acc244aa942ab0f729ed28131b9d1890c37ecc8c..b3390d66a9eac279dc51300543727364c9487648 100644 (file)
--- a/helm/matita/matitaGui.mli
+++ b/helm/matita/matitaGui.mli
@@ -61,10 +61,6 @@ class gui :
       (** prompt the user for a (multiline) text entry *)
     method askText: ?title:string -> ?msg:string -> unit -> string option
 
-      (** lock script text view from the beginning to the given offset (in UTF-8
-      * characters) *)
-    method lockScript: int -> unit
-
   end
 
   (** singleton instance of the gui *)