Matitaweb:

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

diff --git a/matitaB/matita/matitaEngine.ml b/matitaB/matita/matitaEngine.ml
index 734140ad3dc6be656045a2be7c3e6b15c513dbc6..3757b177f1706dc3fc290c8f402a20af3a51dbe0 100644 (file)
--- a/matitaB/matita/matitaEngine.ml
+++ b/matitaB/matita/matitaEngine.ml
@@ -135,7 +135,7 @@ let baseuri_of_script ~include_paths fname =
 let rec get_ast status ~compiling ~asserted ~include_paths strm = 
   match GrafiteParser.parse_statement status strm with
      (GrafiteAst.Executable
-       (_,GrafiteAst.NCommand (_,GrafiteAst.Include (_,_,mafilename)))) as cmd
+       (loc,GrafiteAst.NCommand (_,GrafiteAst.Include (_,_,mafilename)))) as cmd
      ->
        let already_included = NCicLibrary.get_transitively_included status in
        let asserted,_ =
@@ -156,7 +156,6 @@ and eval_from_stream ~compiling ~asserted ~include_paths ?do_heavy_checks status
      match cont with
      | None -> asserted, true, status, str
      | Some (asserted,ast) ->
-        (* pp_ast_statement status ast; *)
         cb status ast;
         let status =
           eval_ast ~include_paths ?do_heavy_checks status ("",0,ast)
@@ -172,7 +171,7 @@ and eval_from_stream ~compiling ~asserted ~include_paths ?do_heavy_checks status
         in
          asserted, false, status, str
    with exn when not matita_debug ->
-     prerr_endline ("EnrichedWithStatus: " ^ Printexc.to_string exn);
+     (* prerr_endline ("EnrichedWithStatus: " ^ Printexc.to_string exn); *)
      raise (EnrichedWithStatus (exn, status))
   in
   if stop then asserted,status else loop asserted status str
@@ -251,13 +250,11 @@ 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;
-     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 
@@ -281,8 +278,8 @@ and assert_ng ~already_included ~compiling ~asserted ~include_paths ?outch ?uid
    let ngtime_of baseuri =
     let ngpath = NCicLibrary.ng_path_of_baseuri uid baseuri in
     let uid = match uid with Some u -> "Some " ^ u | _ -> "None" in
-    prerr_endline ("uid = " ^ uid);
-    prerr_endline ("ngpath = " ^ ngpath);
+    (* prerr_endline ("uid = " ^ uid);
+    prerr_endline ("ngpath = " ^ ngpath); *)
     try
      Some (Unix.stat ngpath).Unix.st_mtime
     with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = ngpath -> None in
@@ -314,7 +311,7 @@ and assert_ng ~already_included ~compiling ~asserted ~include_paths ?outch ?uid
          asserted, children_bad || matime > ngtime
      | None -> asserted,true
    in
-    prerr_endline ("asserted = " ^ (String.concat "," asserted));
+    (* prerr_endline ("asserted = " ^ (String.concat "," asserted)); *)
     if not to_be_compiled then fullmapath::asserted,false
     else
      if List.mem baseuri already_included then
@@ -326,7 +323,7 @@ and assert_ng ~already_included ~compiling ~asserted ~include_paths ?outch ?uid
         | None -> open_out (fullmapath ^ ".mad"), true
         | Some c -> c, false
       in
-      prerr_endline ("compiling " ^ fullmapath);
+      (* prerr_endline ("compiling " ^ fullmapath); *)
       let asserted = compile ~compiling ~asserted ~include_paths ~outch ?uid fullmapath in
        if is_file_ch then close_out outch;
        fullmapath::asserted,true