X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaScript.ml;h=8de5ccebc3dd74f54d218b85ccdf065b7e5ddf77;hb=df1201e37d6f2631dc31ffc87b979a6c81180a3a;hp=05dad0572be58cdc72bb1b650b7be81c3e8c6fe4;hpb=a9e037fe189335607ab5d10523c836d8c7717245;p=helm.git

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index 05dad0572..8de5ccebc 100644
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -105,7 +105,7 @@ let eval_with_engine include_paths guistuff grafite_status user_goal
  * so that we can ensure the inclusion is performed after the included file 
  * is compiled (if needed). matitac does not need that, since it compiles files
  * in the good order, here files may be compiled on demand. *)
-let wrap_with_make include_paths (f : GrafiteParser.statement) x = 
+let wrap_with_make include_paths (f : #LexiconEngine.status GrafiteParser.statement) x = 
   try      
     f ~never_include:true ~include_paths x
   with
@@ -612,12 +612,12 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff
         let ast = 
          wrap_with_make include_paths
           (GrafiteParser.parse_statement (Ulexing.from_utf8_string text)) 
-            (GrafiteTypes.get_lexicon grafite_status)
+            (GrafiteTypes.get_estatus grafite_status)
         in
           ast, text
-    | `Ast (st, text) -> (GrafiteTypes.get_lexicon grafite_status, st), text
+    | `Ast (st, text) -> (GrafiteTypes.get_estatus grafite_status, st), text
   in
-  let grafite_status = GrafiteTypes.set_lexicon lexicon_status grafite_status in
+  let grafite_status = GrafiteTypes.set_estatus lexicon_status grafite_status in
   let text_of_loc floc = 
     let nonskipped_txt,_ = MatitaGtkMisc.utf8_parsed_text unparsed_text floc in
     let start, stop = HExtlib.loc_of_floc floc in 
@@ -675,7 +675,7 @@ let buffer = source_view#buffer in
 let source_buffer = source_view#source_buffer in
 let initial_statuses baseuri =
  let lexicon_status =
-   CicNotation2.load_notation ~include_paths:[]
+   CicNotation2.load_notation ~include_paths:[] (new LexiconEngine.status)
      BuildTimeConf.core_notation_script 
  in
  let grafite_status = GrafiteSync.init lexicon_status baseuri in
@@ -816,8 +816,8 @@ object (self)
     match history with s::_ -> s | [] -> assert false
    in
     LexiconSync.time_travel 
-      ~present:(GrafiteTypes.get_lexicon cur_grafite_status)
-      ~past:(GrafiteTypes.get_lexicon grafite_status);
+      ~present:(GrafiteTypes.get_estatus cur_grafite_status)
+      ~past:(GrafiteTypes.get_estatus grafite_status);
     GrafiteSync.time_travel ~present:cur_grafite_status ~past:grafite_status;
     statements <- new_statements;
     history <- new_history;
@@ -985,8 +985,8 @@ object (self)
      * library_objects.set_default... *)
     GrafiteSync.time_travel ~present:self#grafite_status ~past:grafite_status;
     LexiconSync.time_travel 
-      ~present:(GrafiteTypes.get_lexicon self#grafite_status)
-      ~past:(GrafiteTypes.get_lexicon grafite_status)
+      ~present:(GrafiteTypes.get_estatus self#grafite_status)
+      ~past:(GrafiteTypes.get_estatus grafite_status)
 
   method private reset_buffer = 
     statements <- [];
@@ -1142,7 +1142,7 @@ object (self)
     in
     try
       is_there_only_comments 
-        (GrafiteTypes.get_lexicon self#grafite_status) self#getFuture
+        (GrafiteTypes.get_estatus self#grafite_status) self#getFuture
     with 
     | LexiconEngine.IncludedFileNotCompiled _
     | HExtlib.Localized _