X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaScript.ml;h=e72644d105a6f238703539c4edc7c8c3847a4265;hb=779859f7a9e317e378d258897c289f447adea7ad;hp=108b23237d74e9db01195ffb456a73bbba80b1df;hpb=9a7c77e5c29d764109a104aa629761ba90cb511c;p=helm.git

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index 108b23237..e72644d10 100644
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -605,19 +605,18 @@ script ex loc
 and eval_statement include_paths (buffer : GText.buffer) guistuff 
  grafite_status user_goal script statement
 =
-  let (lexicon_status,st), unparsed_text =
+  let (grafite_status,st), unparsed_text =
     match statement with
     | `Raw text ->
         if Pcre.pmatch ~rex:only_dust_RE text then raise Margin;
         let ast = 
          wrap_with_make include_paths
           (GrafiteParser.parse_statement (Ulexing.from_utf8_string text)) 
-            (GrafiteTypes.get_estatus grafite_status)
+            grafite_status
         in
           ast, text
-    | `Ast (st, text) -> (GrafiteTypes.get_estatus grafite_status, st), text
+    | `Ast (st, text) -> (grafite_status, st), text
   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 
@@ -815,9 +814,7 @@ object (self)
    let cur_grafite_status =
     match history with s::_ -> s | [] -> assert false
    in
-    LexiconSync.time_travel 
-      ~present:(GrafiteTypes.get_estatus cur_grafite_status)
-      ~past:(GrafiteTypes.get_estatus grafite_status);
+    LexiconSync.time_travel ~present:cur_grafite_status ~past:grafite_status;
     GrafiteSync.time_travel ~present:cur_grafite_status ~past:grafite_status;
     statements <- new_statements;
     history <- new_history;
@@ -984,9 +981,7 @@ object (self)
     (* FIXME: this is not correct since there is no undo for 
      * library_objects.set_default... *)
     GrafiteSync.time_travel ~present:self#grafite_status ~past:grafite_status;
-    LexiconSync.time_travel 
-      ~present:(GrafiteTypes.get_estatus self#grafite_status)
-      ~past:(GrafiteTypes.get_estatus grafite_status)
+    LexiconSync.time_travel ~present:self#grafite_status ~past:grafite_status
 
   method private reset_buffer = 
     statements <- [];
@@ -1140,9 +1135,7 @@ object (self)
       | GrafiteParser.LNone _
       | GrafiteParser.LSome (GrafiteAst.Executable _) -> false
     in
-    try
-      is_there_only_comments 
-        (GrafiteTypes.get_estatus self#grafite_status) self#getFuture
+    try is_there_only_comments self#grafite_status self#getFuture
     with 
     | LexiconEngine.IncludedFileNotCompiled _
     | HExtlib.Localized _