X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=0d0fa1ba8c863df9bcd689054eb16a88e8f1f8fa;hb=2b061073ed17c537a6ea969960e5a3038ed30d05;hp=7b73eb112b5b2c5f517711da398f67ec1ca82054;hpb=646ade789430669f4a6be3ecbf47d89fe865f132;p=helm.git

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 7b73eb112..0d0fa1ba8 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -42,7 +42,7 @@ end
 class console ~(buffer: GText.buffer) () =
   object (self)
     val error_tag   = buffer#create_tag [ `FOREGROUND "red" ]
-    val warning_tag = buffer#create_tag [ `FOREGROUND "yellow" ]
+    val warning_tag = buffer#create_tag [ `FOREGROUND "orange" ]
     val message_tag = buffer#create_tag []
     val debug_tag   = buffer#create_tag [ `FOREGROUND "#888888" ]
     method message s = buffer#insert ~iter:buffer#end_iter ~tags:[message_tag] s
@@ -67,9 +67,10 @@ let clean_current_baseuri status =
 
 let ask_and_save_moo_if_needed parent fname status = 
   let save () =
-    MatitacLib.dump_moo_to_file fname status.MatitaTypes.moo_content_rev
-  in
-  if (MatitaScript.instance ())#eos then
+    MatitacLib.dump_moo_to_file fname status.MatitaTypes.moo_content_rev in
+  if (MatitaScript.instance ())#eos &&
+     status.MatitaTypes.proof_status = MatitaTypes.No_proof
+  then
     begin
       let mooname = 
         MatitaMisc.obj_file_of_script fname
@@ -289,7 +290,12 @@ class gui () =
           | None -> ()
         with MatitaTypes.Cancel -> ()
       in
-      let newScript () = (s ())#reset (); disableSave () in
+      let newScript () = 
+        (s ())#reset (); 
+        (s ())#template (); 
+        disableSave ();
+        script_fname <- None
+      in
       let cursor () =
         source_buffer#place_cursor
           (source_buffer#get_iter_at_mark (`NAME "locked"))
@@ -330,7 +336,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;
@@ -377,13 +383,23 @@ class gui () =
       let main_h = height * 80 / 100 in
       let script_w = main_w * 6 / 10 in
       self#main#toplevel#resize ~width:main_w ~height:main_h;
-      self#main#hpaneScriptSequent#set_position script_w  
+      self#main#hpaneScriptSequent#set_position script_w;
+        (* source_view *)
+      ignore(source_view#connect#after#paste_clipboard 
+        ~callback:(fun () -> (MatitaScript.instance ())#clean_dirty_lock))
     
     method loadScript file =       
       let script = MatitaScript.instance () in
       script#reset (); 
       script#assignFileName file;
-      script#loadFromFile (); 
+      if not (Sys.file_exists file) then
+        begin
+          let oc = open_out file in
+          let template = MatitaMisc.input_file BuildTimeConf.script_template in 
+          output_string oc template;
+          close_out oc
+        end;
+      script#loadFromFile ();
       console#message ("'"^file^"' loaded.");
       self#_enableSaveTo file