Bug fixed: added a _undoable_action critical section to the reset method of

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

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index f7094ab95d282763733ab987af03bd7ec28d94f5..bcb715f2dcd8019cd6c70f0a9fe678306495c036 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -415,7 +415,7 @@ let fresh_script_id =
   let i = ref 0 in
   fun () -> incr i; !i
 
-class script  ~(view: GText.view)
+class script  ~(source_view: GSourceView.source_view)
               ~(init: MatitaTypes.status) 
               ~(mathviewer: MatitaTypes.mathViewer) 
               ~set_star
@@ -423,7 +423,8 @@ class script  ~(view: GText.view)
               ~urichooser 
               ~develcreator 
               () =
-let buffer = view#buffer in
+let buffer = source_view#buffer in
+let source_buffer = source_view#source_buffer in
 object (self)
   val scriptId = fresh_script_id ()
   
@@ -553,10 +554,10 @@ object (self)
       | _ -> ()
     end ;
     let mark_position = buffer#get_iter_at_mark mark in
-    if view#move_mark_onscreen mark then
+    if source_view#move_mark_onscreen mark then
      begin
       buffer#move_mark mark mark_position;
-      view#scroll_to_mark ~use_align:true ~xalign:1.0 ~yalign:0.1 mark;
+      source_view#scroll_to_mark ~use_align:true ~xalign:1.0 ~yalign:0.1 mark;
      end;
     while Glib.Main.pending () do ignore(Glib.Main.iteration false); done
 
@@ -612,7 +613,9 @@ object (self)
 
   method reset () =
     self#goto_top;
+    source_buffer#begin_not_undoable_action ();
     buffer#delete ~start:buffer#start_iter ~stop:buffer#end_iter;
+    source_buffer#end_not_undoable_action ();
     self#notify;
     buffer#set_modified false
 
@@ -747,10 +750,10 @@ end
 
 let _script = ref None
 
-let script ~view ~init ~mathviewer ~urichooser ~develcreator ~ask_confirmation ~set_star ()
+let script ~source_view ~init ~mathviewer ~urichooser ~develcreator ~ask_confirmation ~set_star ()
 =
   let s = new script 
-    ~view ~init ~mathviewer ~ask_confirmation ~urichooser ~develcreator ~set_star () 
+    ~source_view ~init ~mathviewer ~ask_confirmation ~urichooser ~develcreator ~set_star () 
   in
   _script := Some s;
   s