X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitaGui.ml;h=3ba6499a93acab767646871f0559dcd6ff848576;hb=fa564a98052e479547a37c9e491623fca5f3e0ba;hp=aae91697a489cdf210649c75803b1b332b0bbbc5;hpb=92e53212b1142355777f171bf683066f52135ed7;p=helm.git

diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml
index aae91697a..3ba6499a9 100644
--- a/matita/matitaGui.ml
+++ b/matita/matitaGui.ml
@@ -1116,35 +1116,17 @@ class gui () =
     method loadScript file =       
       let script = MatitaScript.current () in
       script#reset (); 
-      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 (Some 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 (Some file);
-          let file = script#filename in
-          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
+      script#assignFileName (Some file);
+      let file = script#filename in
+      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
       
     method setStar b =
       let s = MatitaScript.current () in