(no commit message)

[helm.git] / matitaB / matita / matitaEngine.ml

diff --git a/matitaB/matita/matitaEngine.ml b/matitaB/matita/matitaEngine.ml
index 83eb235fb82350d3dd2baa613580d73195c72203..14716e2b68143102be55fa187c63ac6349b781fb 100644 (file)
--- a/matitaB/matita/matitaEngine.ml
+++ b/matitaB/matita/matitaEngine.ml
@@ -156,12 +156,14 @@ and eval_from_stream ~compiling ~asserted ~include_paths ?do_heavy_checks status
      match cont with
      | None -> asserted, true, status
      | Some (asserted,ast) ->
+        (* pp_ast_statement status ast; *)
         cb status ast;
         let status =
           eval_ast ~include_paths ?do_heavy_checks status ("",0,ast)
         in
          asserted, false, status
    with exn when not matita_debug ->
+     prerr_endline ("EnrichedWithStatus: " ^ Printexc.to_string exn);
      raise (EnrichedWithStatus (exn, status))
   in
   if stop then asserted,status else loop asserted status
@@ -172,6 +174,7 @@ and compile ~compiling ~asserted ~include_paths ~outch ?uid fname =
   if List.mem fname compiling then raise (CircularDependency fname);
   let compiling = fname::compiling in
   let matita_debug = Helm_registry.get_bool "matita.debug" in
+  let matita_debug = true in
   let root,baseuri,fname,_tgt = 
     Librarian.baseuri_of_script ~include_paths fname in
   if Http_getter_storage.is_read_only baseuri then assert false;
@@ -211,6 +214,7 @@ and compile ~compiling ~asserted ~include_paths ~outch ?uid fname =
         (Filename.dirname 
           (Http_getter.filename ~local:true ~writable:true (baseuri ^
           "foo.con")));
+    prerr_endline ("trying to compile " ^ fname); 
     let buf =
      GrafiteParser.parsable_statement status
       (Ulexing.from_utf8_channel (open_in fname))
@@ -221,6 +225,7 @@ and compile ~compiling ~asserted ~include_paths ~outch ?uid fname =
     in
     let asserted, status =
      eval_from_stream ~compiling ~asserted ~include_paths status buf print_cb in
+    prerr_endline ("end compile of " ^ fname); 
     let elapsed = Unix.time () -. time in
      (if Helm_registry.get_bool "matita.moo" then begin
        GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
@@ -237,12 +242,13 @@ and compile ~compiling ~asserted ~include_paths ~outch ?uid fname =
      HLog.message 
        (sprintf "execution of %s completed in %s." fname (hou^min^sec));
      pp_times fname true big_bang big_bang_u big_bang_s;
-     (* XXX: update script -- currently to stdout *)
+     prerr_endline ("now generating disambiguated script for " ^ fname);
      let origbuf = Ulexing.from_utf8_channel (open_in fname) in
      let interpr = GrafiteDisambiguate.get_interpr status#disambiguate_db in
      let outstr = ref "" in
      ignore (SmallLexer.mk_small_printer interpr outstr origbuf);
      Printf.fprintf outch "%s" !outstr;
+     prerr_endline ("returning after compilation of " ^ fname);
      asserted
 (* MATITA 1.0: debbo fare time_travel sulla ng_library?
      LexiconSync.time_travel