]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matitaGui.ml
blocked undo of authomatic text (template)
[helm.git] / helm / matita / matitaGui.ml
index 00684d975babda51ef2fd3e0801cc38cc63fe1aa..ac69d2615a902bc822ff656a8a4dcbe543a289a0 100644 (file)
@@ -430,15 +430,19 @@ class gui () =
           | Some f -> 
                 script#reset (); 
                 script#assignFileName f;
+                source_view#source_buffer#begin_not_undoable_action ();
                 script#loadFromFile (); 
+                source_view#source_buffer#end_not_undoable_action ();
                 console#message ("'"^f^"' loaded.\n");
                 self#_enableSaveTo f
           | None -> ()
         with MatitaTypes.Cancel -> ()
       in
       let newScript () = 
+        source_view#source_buffer#begin_not_undoable_action ();
         (s ())#reset (); 
         (s ())#template (); 
+        source_view#source_buffer#end_not_undoable_action ();
         disableSave ();
         script_fname <- None
       in
@@ -563,7 +567,9 @@ class gui () =
           output_string oc template;
           close_out oc
         end;
+      source_view#source_buffer#begin_not_undoable_action ();
       script#loadFromFile ();
+      source_view#source_buffer#end_not_undoable_action ();
       console#message ("'"^file^"' loaded.");
       self#_enableSaveTo file