From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 9 Jan 2008 13:11:22 +0000 (+0000)
Subject: no more matitaprover
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=fa564a98052e479547a37c9e491623fca5f3e0ba

no more matitaprover
---

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
diff --git a/matita/matitac.ml b/matita/matitac.ml
index 6836e44a2..2f2987388 100644
--- 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