From dcb9e3da241393db2a23fd7925cd9543a4034205 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 9 Feb 2005 15:06:25 +0000 Subject: [PATCH] moved lockScript to MatitaScript module --- helm/matita/matitaGui.ml | 16 ---------------- helm/matita/matitaGui.mli | 4 ---- 2 files changed, 20 deletions(-) diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index c1bdfcc77..b67b523f4 100644 --- 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 acc244aa9..b3390d66a 100644 --- 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 *) -- 2.39.2