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 e0e4227dd1f5709d921b4bd57f3bf8b0df6594dd..ad4592a67ec028c545afb948c88e5b51a949464a 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -337,7 +337,7 @@ let eval_executable guistuff status user_goal parsed_text script ex =
         (match ML.baseuri_of_baseuri_decl (TA.Executable (loc,ex)) with
         | None -> ()
         | Some u -> 
-            if not (MatitacleanLib.is_empty u) then
+            if not (ML.is_empty u) then
               match 
                 guistuff.ask_confirmation 
                   ~title:"Baseuri redefinition" 
@@ -417,9 +417,7 @@ object (self)
        (fun _ -> if buffer#modified then 
           set_star self#ppFilename true 
         else 
-          set_star self#ppFilename false));
-    self#reset ();
-    self#template ()
+          set_star self#ppFilename false))
 
   val mutable statements = [];    (** executed statements *)
   val mutable history = [ init ];
@@ -436,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
@@ -611,12 +611,12 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements;
         | exc -> self#notify; raise exc)
     | `Cursor ->
         let locked_iter () = buffer#get_iter_at_mark (`NAME "locked") in
-        let cursor_iter () = buffer#get_iter_at_mark `INSERT in
-        let cmp = (locked_iter ())#offset - (cursor_iter ())#offset in
+        let cursor_iter = buffer#get_iter_at_mark `INSERT in
+        let cmp = (locked_iter ())#offset - cursor_iter#offset in
         let forward_until_cursor () = (* go forward until locked > cursor *)
           let rec aux oldpos =
             self#_advance ();
-            if (locked_iter ())#compare (cursor_iter ()) < 0 &&
+            if (locked_iter ())#compare cursor_iter < 0 &&
                oldpos#compare (getpos ()) < 0 
             then
               aux (getpos ())