Bug fix: undo now respects the locked area.

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

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 5fa044e5330779cd68f58ce1aa1aa27ccde2f67d..ad4592a67ec028c545afb948c88e5b51a949464a 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -434,6 +434,8 @@ object (self)
     buffer#create_mark ~name:"locked" ~left_gravity:true buffer#start_iter
   val locked_tag = buffer#create_tag [`BACKGROUND "lightblue"; `EDITABLE false]
 
+  method locked_mark = locked_mark
+
     (* history can't be empty, the invariant above grant that it contains at
      * least the init status *)
   method status = match history with hd :: _ -> hd | _ -> assert false