From e04169b2712f46b10e1923ff2fea5ebfd775c8dd Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 28 Jun 2005 17:15:02 +0000
Subject: [PATCH] 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
---
helm/matita/{matitatop.bootstrap => .ocamlinit} | 9 ++-------
helm/matita/matitatop.ml | 10 +++++++---
2 files changed, 9 insertions(+), 10 deletions(-)
rename helm/matita/{matitatop.bootstrap => .ocamlinit} (87%)
diff --git a/helm/matita/matitatop.bootstrap b/helm/matita/.ocamlinit
similarity index 87%
rename from helm/matita/matitatop.bootstrap
rename to helm/matita/.ocamlinit
index a9538cf7d..90f438570 100644
--- a/helm/matita/matitatop.bootstrap
+++ b/helm/matita/.ocamlinit
@@ -25,10 +25,5 @@
#install_printer CicMetaSubst.fppterm;;
#install_printer CicMetaSubst.fppmetasenv;;
-(* main *)
-let _ =
- if Array.length Sys.argv > 1 then
- MatitacLib.main `TOPLEVEL
- else
- MatitacLib.go ()
-;;
+(* utility functions *)
+let go = 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
--
2.39.2