From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 28 Jun 2005 17:30:58 +0000 (+0000)
Subject: matitatop.ml is now a simple invocation of Toploop.loop and .ocamlinit is
X-Git-Tag: INDEXING_NO_PROOFS~18
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f14850541c1345e7ca745de6baf89c4639f2b824;p=helm.git

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!
---

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