moved lockScript to MatitaScript module

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index c1bdfcc77f0d46fc5a4b7e0c20d42a901761ba3c..b67b523f46c2db475cfe67c0797ba74a27e04a33 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -45,17 +45,9 @@ class gui file =
       ~phrase_sep:BuildTimeConf.phrase_sep
       ~packing:main#scrolledConsole#add ~paned:main#mainVPanes ()
   in
-  let script_buf = script#scriptTextView#buffer in
   object (self)
     val mutable chosen_file = None
 
-      (** text mark and tag representing locked part of a script *)
-    val locked_mark =
-      script_buf#create_mark ~name:"locked" ~left_gravity:true
-        script_buf#start_iter
-    val locked_tag =
-      script_buf#create_tag [`BACKGROUND "green"; `EDITABLE false]
-
     initializer
         (* glade's check widgets *)
       List.iter (fun w -> w#check_widgets ())
@@ -185,14 +177,6 @@ class gui file =
       GtkThread.main ();
       !text
 
-    method lockScript offset =
-      let mark = `MARK locked_mark in
-      script_buf#move_mark mark ~where:(script_buf#get_iter_at_char offset);
-      script_buf#remove_tag locked_tag ~start:script_buf#start_iter
-        ~stop:script_buf#end_iter;
-      script_buf#apply_tag locked_tag ~start:script_buf#start_iter
-        ~stop:(script_buf#get_iter_at_mark mark)
-
   end
 
 let gui () = new gui (Helm_registry.get "matita.glade_file")

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 *)