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 (file)
index 0000000..90f4385
--- /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 (file)
index a9538cf..0000000
--- 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 95a8ec192e507c90049734a1714d4d3628b4613c..c9bf8d98220275ad48f632ae306cc98411bc0fe8 100644 (file)
--- 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