From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 5 Jul 2005 14:36:47 +0000 (+0000)
Subject: This commit fixes matitatop that was no longer working without arguments.
X-Git-Tag: V_0_7_1~86
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6e7fd1727eafb8280d2a01c05eddf49d19db2aaa;p=helm.git

This commit fixes matitatop that was no longer working without arguments.
It also make matitatop clean everything without exiting, unless the user
types ^D in the ocaml toploop :-(
---

diff --git a/helm/matita/.ocamlinit b/helm/matita/.ocamlinit
index f5c30f839..d1eac4cbd 100644
--- a/helm/matita/.ocamlinit
+++ b/helm/matita/.ocamlinit
@@ -32,7 +32,7 @@ let fppuri ppf uri =
 #install_printer fppuri;;
 
 (* utility functions *)
-let go = MatitacLib.go;;
+let go = MatitacLib.interactive_loop;;
 
 (* let's go! *)
 let _ = 
diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml
index ec722490a..d4bd0aafe 100644
--- a/helm/matita/matitacLib.ml
+++ b/helm/matita/matitacLib.ml
@@ -81,40 +81,44 @@ let pp_ocaml_mode () =
   MatitaLog.message "Type 'go ();;' to enter an interactive matitac";
   MatitaLog.message ""
   
-let rec go () = 
+let clean_exit n =
+ match !status with
+    None -> exit n
+  | Some status ->
+     let baseuri = MatitaTypes.get_string_option !status "baseuri" in
+      MatitacleanLib.clean_baseuris ~verbose:false [baseuri];
+      exit n
+  
+let rec interactive_loop () = 
  let str = Stream.of_channel stdin in
   try
     run_script str MatitaEngine.eval_from_stream_greedy
   with 
   | MatitaEngine.Drop -> pp_ocaml_mode ()
-  | Sys.Break -> MatitaLog.error "user break!"; go ()
-  | MatitaTypes.Command_error _ -> go ()
+  | Sys.Break -> MatitaLog.error "user break!"; interactive_loop ()
+  | MatitaTypes.Command_error _ -> interactive_loop ()
   | CicTextualParser2.Parse_error (floc,err) ->
      (* check for EOI *)
      if Stream.peek str = None then
-      exit 0
+      clean_exit 0
      else
       let (x, y) = CicAst.loc_of_floc floc in
       MatitaLog.error (sprintf "Parse error at %d-%d: %s" x y err);
-      go ()
-  | exn -> MatitaLog.error (Printexc.to_string exn); go ()
+      interactive_loop ()
+  | exn -> MatitaLog.error (Printexc.to_string exn); interactive_loop ()
+
+let go () =
+  Helm_registry.load_from "matita.conf.xml";
+  Http_getter.init ();
+  MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
+  status := Some (ref (Lazy.force MatitaEngine.initial_status));
+  Sys.catch_break true;
+  interactive_loop ()
 
-let clean_exit n =
- match !status with
-    None -> exit n
-  | Some status ->
-     let baseuri = MatitaTypes.get_string_option !status "baseuri" in
-      MatitacleanLib.clean_baseuris ~verbose:false [baseuri];
-      exit n
-  
 let main ~mode = 
   Helm_registry.load_from "matita.conf.xml";
   Http_getter.init ();
   MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
-(*
-  MatitaDb.clean_owner_environment ();
-  MatitaDb.create_owner_environment ();
-*)
   status := Some (ref (Lazy.force MatitaEngine.initial_status));
   Sys.catch_break true;
   let fname = fname () in
diff --git a/helm/matita/matitacLib.mli b/helm/matita/matitacLib.mli
index b778b91f3..8032320ce 100644
--- a/helm/matita/matitacLib.mli
+++ b/helm/matita/matitacLib.mli
@@ -23,5 +23,13 @@
  * http://helm.cs.unibo.it/
  *)
 
+val interactive_loop : unit -> unit
+
+(** go initializes the status and calls interactive_loop *)
 val go : unit -> unit
 val main : mode:[ `COMPILER | `TOPLEVEL ] -> unit
+
+(** clean_exit n
+  performs an exit [n] after a complete clean-up of what was partially compiled
+*)
+val clean_exit : int -> unit
diff --git a/helm/matita/matitatop.ml b/helm/matita/matitatop.ml
index 9e1698009..947b43b25 100644
--- a/helm/matita/matitatop.ml
+++ b/helm/matita/matitatop.ml
@@ -1,3 +1,4 @@
 let _ =
   let _ = Topdirs.dir_quit in
-  Toploop.loop Format.std_formatter
+  Toploop.loop Format.std_formatter;
+  assert false