X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitaGui.ml;h=7270603a9636b7ebcd4be445ce9350b0757dfefb;hb=fe9fe2e62685608b6294b841fd6887a4bf99c812;hp=b1b2a6ad3fa683c2856a9f4226bd547077534365;hpb=834f4ec558838456604312b605bdce3a5d099403;p=helm.git

diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml
index b1b2a6ad3..7270603a9 100644
--- a/matita/matitaGui.ml
+++ b/matita/matitaGui.ml
@@ -612,7 +612,7 @@ class gui () =
         (tac_w_term (A.Transitivity (loc, hole)));
       connect_button tbar#assumptionButton (tac (A.Assumption loc));
       connect_button tbar#cutButton (tac_w_term (A.Cut (loc, None, hole)));
-      connect_button tbar#autoButton (tac (A.Auto (loc,None,None,None,None)));
+      connect_button tbar#autoButton (tac (A.Auto (loc,[])));
       MatitaGtkMisc.toggle_widget_visibility
        ~widget:(main#tacticsButtonsHandlebox :> GObj.widget)
        ~check:main#tacticsBarMenuItem;
@@ -1007,16 +1007,34 @@ class gui () =
     method loadScript file =       
       let script = MatitaScript.current () in
       script#reset (); 
-      script#assignFileName file;
-      let content =
-       if Sys.file_exists file then file
-       else BuildTimeConf.script_template
-      in
-       source_view#source_buffer#begin_not_undoable_action ();
-       script#loadFromFile content;
-       source_view#source_buffer#end_not_undoable_action ();
-       console#message ("'"^file^"' loaded.");
-       self#_enableSaveTo file
+      if Pcre.pmatch ~pat:"\\.p$" file then
+        begin
+          let tptppath = 
+            Helm_registry.get_opt_default Helm_registry.string ~default:"./"
+              "matita.tptppath"
+          in
+          let data = Matitaprover.p_to_ma ~filename:file ~tptppath () in
+          let filename = Pcre.replace ~pat:"\\.p$" ~templ:".ma" file in
+          script#assignFileName filename;
+          source_view#source_buffer#begin_not_undoable_action ();
+          script#loadFromString data;
+          source_view#source_buffer#end_not_undoable_action ();
+          console#message ("'"^filename^"' loaded.");
+          self#_enableSaveTo filename
+        end
+      else
+        begin
+          script#assignFileName file;
+          let content =
+           if Sys.file_exists file then file
+           else BuildTimeConf.script_template
+          in
+           source_view#source_buffer#begin_not_undoable_action ();
+           script#loadFromFile content;
+           source_view#source_buffer#end_not_undoable_action ();
+           console#message ("'"^file^"' loaded.");
+           self#_enableSaveTo file
+        end
       
     method setStar name b =
       let l = main#scriptLabel in