include statement better implemented:

[helm.git] / helm / software / matita / matitaScript.ml

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index a92b5b789707020df7c05b9de48ed906693cfe66..0234c4824673837682dae785401920ab7abcd0ad 100644 (file)
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -118,23 +118,14 @@ let wrap_with_make include_paths (f : GrafiteParser.statement) x =
           HLog.error "please create it.";
           raise (Failure ("No root file for "^mafilename))
       in
-      let initial_lexicon_status = 
-        CicNotation2.load_notation ~include_paths:[] BuildTimeConf.core_notation_script 
-      in
-      let b,x = 
+      let b = 
         try
           GrafiteSync.push ();
-          LexiconSync.time_travel ~present:x ~past:initial_lexicon_status;
+          LexiconSync.push ();
           let rc = MatitacLib.Make.make root [tgt] in 
+          LexiconSync.pop ();
           GrafiteSync.pop ();
-          CicNotation.reset ();
-          ignore(CicNotation2.load_notation ~include_paths:[]
-            BuildTimeConf.core_notation_script);
-          let x = List.fold_left (fun s c -> LexiconEngine.eval_command s c)
-            initial_lexicon_status (List.rev
-            x.LexiconEngine.lexicon_content_rev) 
-          in
-          rc,x
+          rc
         with 
         | exn ->
             HLog.error ("Unexpected " ^ snd(MatitaExcPp.to_string exn));