The getter maps are now dumped also if matitac exits abruptly.

[helm.git] / helm / matita / matitac.ml

diff --git a/helm/matita/matitac.ml b/helm/matita/matitac.ml
index bb796db1e79d8f005630d227cfacd8bdee3437a7..b3767c5397cf3477ad62c607f9df011a0e8d48bb 100644 (file)
--- a/helm/matita/matitac.ml
+++ b/helm/matita/matitac.ml
@@ -1,4 +1,4 @@
-(* Copyright (C) 2004, HELM Team.
+(* Copyright (C) 2004-2005, HELM Team.
  * 
  * This file is part of HELM, an Hypertextual, Electronic
  * Library of Mathematics, developed at the Computer Science
@@ -27,27 +27,6 @@ open Printf
 
 open MatitaTypes
 
-let message s = printf  "** MatitaC: %s\n" s; flush stdout
-let warn s =    eprintf "** MatitaC WARNING: %s\n" s; flush stdout
-let error s =   eprintf "** MatitaC ERROR: %s\n" s; flush stderr
-
-  (** console which prints on stdout/stderr *)
-class tty_console =
-  object (self)
-    method clear () = ()
-    method echo_message s = message s
-    method echo_error s =  error s
-      (* TODO Zack: this method is similar to omonymous method in console,
-      * factorize it in a common super class *)
-    method wrap_exn: 'a. (unit -> 'a) -> 'a option =
-      fun f ->
-      try
-        Some (f ())
-      with exn ->
-        self#echo_error (explain exn);
-        None
-  end
-
 (** {2 Initialization} *)
 
 let arg_spec = [
@@ -57,7 +36,12 @@ let usage =
   sprintf "MatitaC v%s\nUsage: matitac [option ...] file ...\nOptions:"
     BuildTimeConf.version
 
-let _ = Helm_registry.load_from "matita.conf.xml"
+let _ =
+  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 ()
 
 let scripts =
   let acc = ref [] in
@@ -65,57 +49,63 @@ let scripts =
   Arg.parse arg_spec add_script usage;
   List.rev !acc
 
-let parserr = new MatitaDisambiguator.parserr ()
-let dbd =
-  Mysql.quick_connect
-    ~host:(Helm_registry.get "db.host")
-    ~user:(Helm_registry.get "db.user")
-    ~database:(Helm_registry.get "db.database")
-    ()
-let _ = MetadataDb.clean ~dbd ~owner:(Helm_registry.get "matita.owner")
-let disambiguator =
-  new MatitaDisambiguator.disambiguator ~parserr ~dbd
-    ~chooseUris:mono_uris_callback ~chooseInterp:mono_interp_callback
-    ()
-let console = new tty_console
-let currentProof = (new MatitaProof.currentProof :> MatitaTypes.currentProof)
-let interpreter =
-  new MatitaInterpreter.interpreter
-    ~disambiguator ~currentProof ~console ~dbd ()
-
 let run_script fname =
-  message (sprintf "execution of %s started:" fname);
-  let script =
-    let ic = open_in fname in
-    let ast = 
-      try 
-        snd (CicTextualParser2.parse_script (Stream.of_channel ic)) 
-      with
-        exn -> 
-          error (explain exn); 
-          assert false (* should be something like (Unix.exit 1) *)
-    in
-    close_in ic;
-    ast
+  let is =
+    Stream.of_channel
+      (match fname with
+      | "stdin" -> stdin
+      | fname -> open_in fname)
   in
-  let rec aux = function
-    | [] -> ()  (* script is over *)
-    | DisambiguateTypes.Comment _ :: tl -> aux tl
-    | DisambiguateTypes.Command ast :: tl ->
-        let loc =
-          match ast with
-          | TacticAst.LocatedTactical (loc, _) -> loc
-          | _ -> assert false
-        in
-        let (success, _) = interpreter#evalAst ast in
-        if not success then
-          error (sprintf "%s: error at %s, aborting." fname
-            (CicAst.pp_location loc))
-        else
-          aux tl
+  let status = ref (Lazy.force MatitaEngine.initial_status) in
+  let slash_n_RE = Pcre.regexp "\\n" in
+  let cb status stm = 
+    (* dump_status status; *)
+    let stm = TacticAstPp.pp_statement stm in
+    let stm = Pcre.replace ~rex:slash_n_RE stm in
+    let stm = 
+      if String.length stm > 50 then
+        String.sub stm 0 50 ^ " ..."
+      else
+        stm
+    in
+    MatitaLog.debug ("Executing: ``" ^ stm ^ "''")
   in
-  aux script;
-  message (sprintf "execution of %s completed." fname)
-
-let _ = List.iter run_script scripts
-
+  try
+    status := MatitaEngine.eval_from_stream !status is cb
+  with
+  | CicTextualParser2.Parse_error (floc,err) ->
+     let (x, y) = CicAst.loc_of_floc floc in
+     MatitaLog.message (sprintf "Parse error at %d-%d: %s" x y err);
+     Http_getter.sync_dump_file ();
+     exit 1
+  | exn -> 
+      MatitaLog.error (Printexc.to_string exn);
+      raise exn
+        
+let _ = 
+  at_exit
+    (fun () ->
+       Http_getter_logger.log "Sync map tree to disk...";
+       Http_getter.sync_dump_file ();
+       print_endline "\nThanks for using Matita!\n");
+  Sys.catch_break true;
+  try
+   List.iter (fun fname -> 
+    let time = Unix.time () in
+    MatitaLog.message (sprintf "execution of %s started:" fname);
+    run_script fname;
+    let elapsed = Unix.time () -. time in
+    let tm = Unix.gmtime elapsed in
+    let sec = 
+      if tm.Unix.tm_sec > 0 then  (string_of_int tm.Unix.tm_sec ^ "''") else "" 
+    in
+    let min = 
+      if tm.Unix.tm_min > 0 then  (string_of_int tm.Unix.tm_min ^ "' ") else "" 
+    in
+    let hou = 
+      if tm.Unix.tm_hour > 0 then (string_of_int tm.Unix.tm_hour ^ "h ") else "" 
+    in
+    MatitaLog.message 
+      (sprintf "execution of %s completed in %s." fname (hou^min^sec))) scripts;
+    exit(0)
+  with Sys.Break -> exit (-1)