From e04169b2712f46b10e1923ff2fea5ebfd775c8dd Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen 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