From f14850541c1345e7ca745de6baf89c4639f2b824 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 28 Jun 2005 17:30:58 +0000 Subject: [PATCH] matitatop.ml is now a simple invocation of Toploop.loop and .ocamlinit is responsible to call MatitacLib.go or MatitacLib.main. Cons: .ocamlinit is more dirty Pros: it is possible to trace something even before doing a drop! --- helm/matita/.ocamlinit | 8 ++++++++ helm/matita/matitatop.ml | 8 +------- 2 files changed, 9 insertions(+), 7 deletions(-) diff --git a/helm/matita/.ocamlinit b/helm/matita/.ocamlinit index 90f438570..ba19e4e2d 100644 --- a/helm/matita/.ocamlinit +++ b/helm/matita/.ocamlinit @@ -27,3 +27,11 @@ (* utility functions *) let go = MatitacLib.go;; + +(* let's go! *) +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 c9bf8d982..9e1698009 100644 --- a/helm/matita/matitatop.ml +++ b/helm/matita/matitatop.ml @@ -1,9 +1,3 @@ let _ = let _ = Topdirs.dir_quit in - let _ = - if Array.length Sys.argv > 1 then - MatitacLib.main `TOPLEVEL - else - MatitacLib.go () - in - Toploop.loop Format.std_formatter + Toploop.loop Format.std_formatter -- 2.39.2