no more matitaprover

[helm.git] / matita / matitaGui.ml

diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml
index aae91697a489cdf210649c75803b1b332b0bbbc5..3ba6499a93acab767646871f0559dcd6ff848576 100644 (file)
--- 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