X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fmatitac.ml;h=4dbac36539ac238afd0ddcc8f6e8a73d477211bf;hb=cba366ace3c62fd66f99addce68ae0e243622b68;hp=533bbc6a3d46df166290596df4da29ed2a745ae4;hpb=ab336f7c09d052c45a09dd49e9b75a39e8b57e5b;p=helm.git

diff --git a/helm/matita/matitac.ml b/helm/matita/matitac.ml
index 533bbc6a3..4dbac3653 100644
--- 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,29 +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
-    method show ?(msg = "") () = assert false; ()
-    method choose_uri (uris: string list): string = assert false
-  end
-
 (** {2 Initialization} *)
 
 let arg_spec = [
@@ -72,42 +49,41 @@ let scripts =
   Arg.parse arg_spec add_script usage;
   List.rev !acc
 
-let console = new tty_console
-let interpreter = MatitaInterpreter.interpreter ~console ()
-
 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
-  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
+  MatitaLog.message (sprintf "execution of %s started:" fname);
+  let is =
+    Stream.of_channel
+      (match fname with
+      | "stdin" -> stdin
+      | fname -> open_in fname)
   in
-  aux script;
-  message (sprintf "execution of %s completed." fname)
+  let status = ref (Lazy.force MatitaEngine.initial_status) in
+  try
+    while true do
+      dump_status !status;
+      try
+        status := MatitaEngine.eval_from_stream !status is
+      with
+      | CicTextualParser2.Parse_error _ as exn -> 
+          try 
+            Stream.empty is; 
+            raise  End_of_file
+          with Stream.Failure -> raise exn
+      | exn -> 
+          MatitaLog.error (Printexc.to_string exn);
+          raise exn
+    done
+  with 
+    | End_of_file ->
+        MatitaLog.message (sprintf "execution of %s completed." fname);
+        Http_getter.sync_dump_file ();
+        exit(0)
+    | 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
+        
 
 let _ = List.iter run_script scripts