added script template

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

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 7b73eb112b5b2c5f517711da398f67ec1ca82054..c3e169c50a371c39051cc7b9863484cfc2f00053 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -289,7 +289,11 @@ class gui () =
           | None -> ()
         with MatitaTypes.Cancel -> ()
       in
-      let newScript () = (s ())#reset (); disableSave () in
+      let newScript () = 
+        (s ())#reset (); 
+        (s ())#template (); 
+        disableSave () 
+      in
       let cursor () =
         source_buffer#place_cursor
           (source_buffer#get_iter_at_mark (`NAME "locked"))
@@ -330,7 +334,7 @@ class gui () =
         else 
           begin  
             (match script_fname with
-            | None -> clean_current_baseuri status 
+            | None -> clean_current_baseuri status; GMain.Main.quit ()
             | Some fname ->
                 try
                   ask_and_save_moo_if_needed main#toplevel fname status;