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 f5c30f839a48a2067c2cea18122352c35f439bd9..d1eac4cbd8f1e4567ec8b9aae8686e20685acd4c 100644 (file)
--- 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 ec722490ab07863238622c7e1f0d2cda14ddbaa9..d4bd0aafe1eef14358c33ca2bdc854a8a7ec4b8d 100644 (file)
--- 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 b778b91f3e80457fadac61afdbcca9b8095fd001..8032320ce7103b487da2e048155ef9e631629d31 100644 (file)
--- 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 9e1698009cbbd908ed127632069645cb5734d946..947b43b2523b368c40332498b673eed97445301a 100644 (file)
--- 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