From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 27 Feb 2013 20:19:28 +0000 (+0000)
Subject: Quick patch: the maxmeta is now pushed/popped when compiling an external file.
X-Git-Tag: make_still_working~1239
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=d655ee5d9a4c4dc99c559556fb494c549574b1ce

Quick patch: the maxmeta is now pushed/popped when compiling an external file.
This is implemented imperatively for now. It should go into a status.
---

diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml
index 06b0da338..5b9b070bc 100644
--- a/matita/matita/matitaEngine.ml
+++ b/matita/matita/matitaEngine.ml
@@ -241,6 +241,9 @@ 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 =
@@ -305,17 +308,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