no more matitaprover

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

diff --git a/matita/matitac.ml b/matita/matitac.ml
index 6836e44a296c6a110216bedae900b092693ce4bc..2f2987388dd34a002ca123f6e0589211980c10cf 100644 (file)
--- a/matita/matitac.ml
+++ b/matita/matitac.ml
@@ -123,7 +123,6 @@ let main () =
   let bin = Filename.basename Sys.argv.(0) in
   if      Pcre.pmatch ~pat:"^matitadep"    bin then Matitadep.main ()
   else if Pcre.pmatch ~pat:"^matitaclean"  bin then Matitaclean.main ()
-  else if Pcre.pmatch ~pat:"^matitaprover" bin then Matitaprover.main ()
   else if Pcre.pmatch ~pat:"^matitawiki"   bin then MatitaWiki.main ()
   else
     let dump_msg = "<filename> Dump with expanded macros to <filename>" in