X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitacLib.ml;fp=matita%2Fmatita%2FmatitacLib.ml;h=84606564547305589be35f4a2b9121c0d2dd7eb1;hb=9369b99d37875350d949661f91403f738e7bf732;hp=5ae5dbf3b4a1dc8d08a7b97fbb3505dda0825392;hpb=de367d0ba895c320f5374d244efe5d10654068d1;p=helm.git

diff --git a/matita/matita/matitacLib.ml b/matita/matita/matitacLib.ml
index 5ae5dbf3b..846065645 100644
--- a/matita/matita/matitacLib.ml
+++ b/matita/matita/matitacLib.ml
@@ -113,17 +113,14 @@ let activate_extraction baseuri fname =
       *)
 ;;
 
-let compile atstart options fname =
+let compile options fname =
   let matita_debug = Helm_registry.get_bool "matita.debug" in
   let include_paths = get_include_paths options 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;
   activate_extraction baseuri fname ;
-  let lexicon_status = new GrafiteDisambiguate.status in
-  atstart (); (* FG: do not invoke before loading the core notation script *)  
-  let grafite_status =
-   (new GrafiteTypes.status baseuri)#set_disambiguate_db lexicon_status#disambiguate_db in
+  let grafite_status = new GrafiteTypes.status baseuri in
   let big_bang = Unix.gettimeofday () in
   let { Unix.tms_utime = big_bang_u ; Unix.tms_stime = big_bang_s} = 
     Unix.times () 
@@ -258,18 +255,18 @@ module F =
 
     let build options fname =
       let matita_debug = Helm_registry.get_bool "matita.debug" in
-      let compile atstart opts fname =
+      let compile opts fname =
         try
         (* MATITA 1.0: c'erano le push/pop per il parser; ma per
          * l'environment nuovo? *)
-         compile atstart opts fname
+         compile opts fname
         with 
         | Sys.Break -> false
         | exn when not matita_debug ->
             HLog.error ("Unexpected " ^ snd(MatitaExcPp.to_string exn));
             assert false
       in
-       compact (compile ignore options fname)
+       compact (compile options fname)
     ;;
 
     let load_deps_file = Librarian.load_deps_file;;