blocked undo of authomatic text (template)

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index db0fd2b18e7ec0be350aecbea58d29dc16745933..1bfd5e51e4578f06605d8aeaf6a748f69638860b 100644 (file)
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -72,26 +72,34 @@ let _ =
     (MatitaGui.interactive_interp_choice ())
 
 let script =
-  MatitaScript.script 
-    ~view:(gui#sourceView :> GText.view)
-    ~init:(Lazy.force MatitaEngine.initial_status) 
-    ~mathviewer:(MatitaMathView.mathViewer ())
-    ~urichooser:(fun uris ->
-      try
-        MatitaGui.interactive_uri_choice ~selection_mode:`SINGLE
-        ~title:"Matita: URI chooser" 
-        ~msg:"Select the URI" ~hide_uri_entry:true
-        ~hide_try:true ~ok_label:"_Apply" ~ok_action:`SELECT
-        ~copy_cb:(fun s -> gui#sourceView#buffer#insert ("\n"^s^"\n"))
-        () ~id:"boh?" uris
-      with MatitaTypes.Cancel -> [])
-    ~set_star:gui#setStar
-    ~ask_confirmation:
-      (fun ~title ~message -> 
-          MatitaGtkMisc.ask_confirmation ~title ~message 
-          ~parent:gui#main#toplevel ())
-    ~develcreator:gui#createDevelopment
-    ()
+  let s = 
+    MatitaScript.script 
+      ~view:(gui#sourceView :> GText.view)
+      ~init:(Lazy.force MatitaEngine.initial_status) 
+      ~mathviewer:(MatitaMathView.mathViewer ())
+      ~urichooser:(fun uris ->
+        try
+          MatitaGui.interactive_uri_choice ~selection_mode:`SINGLE
+          ~title:"Matita: URI chooser" 
+          ~msg:"Select the URI" ~hide_uri_entry:true
+          ~hide_try:true ~ok_label:"_Apply" ~ok_action:`SELECT
+          ~copy_cb:(fun s -> gui#sourceView#buffer#insert ("\n"^s^"\n"))
+          () ~id:"boh?" uris
+        with MatitaTypes.Cancel -> [])
+      ~set_star:gui#setStar
+      ~ask_confirmation:
+        (fun ~title ~message -> 
+            MatitaGtkMisc.ask_confirmation ~title ~message 
+            ~parent:gui#main#toplevel ())
+      ~develcreator:gui#createDevelopment
+      ()
+  in
+  gui#sourceView#source_buffer#begin_not_undoable_action ();
+  s#reset (); 
+  s#template (); 
+  gui#sourceView#source_buffer#end_not_undoable_action ();
+  s
+  
 
   (* math viewers *)
 let _ =

diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt
index b882d4d0ad73b904a4d134c0826b1a609715d9f1..92626557c11550148ccb4eb6485bb8e05cf3f5c1 100644 (file)
--- a/helm/matita/matita.txt
+++ b/helm/matita/matita.txt
@@ -82,7 +82,9 @@ TODO
     directory .matita
   - notazione -> Luca e Zack
   - copiare nel .moo la baseuri e poi il matitaclean la legge da li e non dal
-    .ma (si evita il syntax error)
+    .ma (si evita il syntax error e il cambio di una baseuri non causa 
+    sporcizia)
+  - non chiudere transitivamente i moo ?? 
 
 DONE
 - gestione dei path per include: il path deve essere assoluto? da decidere ...

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 00684d975babda51ef2fd3e0801cc38cc63fe1aa..ac69d2615a902bc822ff656a8a4dcbe543a289a0 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -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
       

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 821602dcecfd3d591d40b5baf95127b435b84746..5fa044e5330779cd68f58ce1aa1aa27ccde2f67d 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -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 ];