From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 28 Jun 2005 17:15:02 +0000 (+0000)
Subject: New solution: instead of using matitatop.bootstrap we prefer a local .ocamlinit.
X-Git-Tag: INDEXING_NO_PROOFS~20
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e04169b2712f46b10e1923ff2fea5ebfd775c8dd;p=helm.git

New solution: instead of using matitatop.bootstrap we prefer a local .ocamlinit.
 Pro:  no need of doing the weird "#use matitatop.bootstrap" by playing with
       ocaml internals.
 Pro:  local definitions and #opens in matitatop.bootstrap were lost. They are
       preserved in .ocamlinit.
 Cons: .ocamlinit must be in "." or in $HOME
 Cons: it can interfere with other .ocamlinit
---

diff --git a/helm/matita/.ocamlinit b/helm/matita/.ocamlinit
new file mode 100644
index 000000000..90f438570
--- /dev/null
+++ b/helm/matita/.ocamlinit
@@ -0,0 +1,29 @@
+(* directories *)
+#directory "../ocaml/cic"
+#directory "../ocaml/cic_notation"
+#directory "../ocaml/cic_omdoc"
+#directory "../ocaml/cic_proof_checking"
+#directory "../ocaml/cic_textual_parser2"
+#directory "../ocaml/cic_transformations"
+#directory "../ocaml/cic_unification"
+#directory "../ocaml/getter"
+#directory "../ocaml/hbugs"
+#directory "../ocaml/mathql"
+#directory "../ocaml/mathql_generator"
+#directory "../ocaml/mathql_interpreter"
+#directory "../ocaml/metadata"
+#directory "../ocaml/paramodulation"
+#directory "../ocaml/registry"
+#directory "../ocaml/tactics"
+#directory "../ocaml/thread"
+#directory "../ocaml/urimanager"
+#directory "../ocaml/xml"
+#directory "../ocaml/xmldiff"
+
+(* custom printers *)
+#install_printer CicMetaSubst.fppsubst;;
+#install_printer CicMetaSubst.fppterm;;
+#install_printer CicMetaSubst.fppmetasenv;;
+
+(* utility functions *)
+let go = MatitacLib.go;;
diff --git a/helm/matita/matitatop.bootstrap b/helm/matita/matitatop.bootstrap
deleted file mode 100644
index a9538cf7d..000000000
--- a/helm/matita/matitatop.bootstrap
+++ /dev/null
@@ -1,34 +0,0 @@
-(* directories *)
-#directory "../ocaml/cic"
-#directory "../ocaml/cic_notation"
-#directory "../ocaml/cic_omdoc"
-#directory "../ocaml/cic_proof_checking"
-#directory "../ocaml/cic_textual_parser2"
-#directory "../ocaml/cic_transformations"
-#directory "../ocaml/cic_unification"
-#directory "../ocaml/getter"
-#directory "../ocaml/hbugs"
-#directory "../ocaml/mathql"
-#directory "../ocaml/mathql_generator"
-#directory "../ocaml/mathql_interpreter"
-#directory "../ocaml/metadata"
-#directory "../ocaml/paramodulation"
-#directory "../ocaml/registry"
-#directory "../ocaml/tactics"
-#directory "../ocaml/thread"
-#directory "../ocaml/urimanager"
-#directory "../ocaml/xml"
-#directory "../ocaml/xmldiff"
-
-(* custom printers *)
-#install_printer CicMetaSubst.fppsubst;;
-#install_printer CicMetaSubst.fppterm;;
-#install_printer CicMetaSubst.fppmetasenv;;
-
-(* main *)
-let _ = 
-  if Array.length Sys.argv > 1 then
-    MatitacLib.main `TOPLEVEL
-  else
-    MatitacLib.go ()
-;;
diff --git a/helm/matita/matitatop.ml b/helm/matita/matitatop.ml
index 95a8ec192..c9bf8d982 100644
--- a/helm/matita/matitatop.ml
+++ b/helm/matita/matitatop.ml
@@ -1,5 +1,9 @@
 let _ =
   let _ = Topdirs.dir_quit in
-  Toploop.initialize_toplevel_env ();
-  Topdirs.dir_use Format.std_formatter "matitatop.bootstrap";
-  Toploop.loop Format.std_formatter
+  let _ = 
+   if Array.length Sys.argv > 1 then
+     MatitacLib.main `TOPLEVEL
+   else
+     MatitacLib.go ()
+  in
+   Toploop.loop Format.std_formatter