Most warnings turned into errors and avoided

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

diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml
index a8e47b562dfb972a86151a132dc984cbf07fedc4..2963e71c45e2cf5c8f4312b9a7c58d48f9ada72e 100644 (file)
--- a/matita/matita/matitaEngine.ml
+++ b/matita/matita/matitaEngine.ml
@@ -25,8 +25,6 @@
 
 (* $Id$ *)
 
-module G = GrafiteAst
-open GrafiteTypes
 open Printf
 
 class status baseuri =
@@ -163,7 +161,7 @@ let baseuri_of_script ~include_paths fname =
 
 (* given a path to a ma file inside the include_paths, returns the
    new include_paths associated to that file *)
-let read_include_paths ~include_paths file =
+let read_include_paths ~include_paths:_ file =
  try 
    let root, _buri, _fname, _tgt = 
      Librarian.baseuri_of_script ~include_paths:[] file in 
@@ -241,12 +239,15 @@ and compile ~compiling ~asserted ~include_paths fname =
   if Http_getter_storage.is_read_only baseuri then assert false;
   (* MATITA 1.0: debbo fare time_travel sulla ng_library? *)
   let status = new status baseuri in
+  (*CSC: bad, one imperative bit is still there!
+         to be moved into functional status *)
+  NCicMetaSubst.pushmaxmeta ();
   let ocamldirname = Filename.dirname fname in
   let ocamlfname = Filename.chop_extension (Filename.basename fname) in
   let status,ocamlfname =
    Common.modname_of_filename status false ocamlfname in
   let ocamlfname = ocamldirname ^ "/" ^ ocamlfname ^ ".ml" in
-  let status = OcamlExtractionTable.open_file status ~baseuri ocamlfname in
+  let status = OcamlExtraction.open_file status ~baseuri ocamlfname in
   let big_bang = Unix.gettimeofday () in
   let { Unix.tms_utime = big_bang_u ; Unix.tms_stime = big_bang_s} = 
     Unix.times () 
@@ -288,7 +289,7 @@ and compile ~compiling ~asserted ~include_paths fname =
     in
     let asserted, status =
      eval_from_stream ~compiling ~asserted ~include_paths status buf print_cb in
-    let status = OcamlExtractionTable.close_file status in
+    let status = OcamlExtraction.close_file status in
     let elapsed = Unix.time () -. time in
      (if Helm_registry.get_bool "matita.moo" then begin
        GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
@@ -305,17 +306,23 @@ and compile ~compiling ~asserted ~include_paths fname =
      HLog.message 
        (sprintf "execution of %s completed in %s." fname (hou^min^sec));
      pp_times s fname true big_bang big_bang_u big_bang_s;
-     asserted
+     (*CSC: bad, one imperative bit is still there!
+            to be moved into functional status *)
+     NCicMetaSubst.pushmaxmeta ();
 (* MATITA 1.0: debbo fare time_travel sulla ng_library?
      LexiconSync.time_travel 
        ~present:lexicon_status ~past:initial_lexicon_status;
-*))
+*)
+     asserted)
   with 
   (* all exceptions should be wrapped to allow lexicon-undo (LS.time_travel) *)
   | exn when not matita_debug ->
 (* MATITA 1.0: debbo fare time_travel sulla ng_library?
        LexiconSync.time_travel ~present:lexicon ~past:initial_lexicon_status;
  *       *)
+      (*CSC: bad, one imperative bit is still there!
+             to be moved into functional status *)
+      NCicMetaSubst.pushmaxmeta ();
       pp_times s fname false big_bang big_bang_u big_bang_s;
       clean_exit baseuri exn
 
@@ -351,10 +358,13 @@ and assert_ng ~already_included ~compiling ~asserted ~include_paths mapath =
         let preamble = GrafiteTypes.Serializer.dependencies_of baseuri in
         let asserted,children_bad =
          List.fold_left
-          (fun (asserted,b) mapath ->
-            let asserted,b1 =
-              assert_ng ~already_included ~compiling ~asserted ~include_paths
-               mapath
+          (fun (asserted,b) mapath -> 
+           let asserted,b1 =
+              try 
+              assert_ng ~already_included ~compiling ~asserted ~include_paths
+                mapath
+             with Librarian.NoRootFor _ | Librarian.FileNotFound _ ->
+               asserted, true 
             in
              asserted, b || b1
               || let _,baseuri,_,_ =