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

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index 8de5ccebc..e72644d10 100644
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -485,7 +485,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff grafite_status
       in
       let t_and_ty = Cic.Cast (term,ty) in
       guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv));
-      [({grafite_status with proof_status = No_proof}), parsed_text ],"", 
+      [(grafite_status#set_proof_status No_proof), parsed_text ],"", 
         parsed_text_length 
   | TA.Check (_,term) ->
       let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in
@@ -512,7 +512,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff grafite_status
         let (_,menv,subst,_,_,_), _ = 
           ProofEngineTypes.apply_tactic
             (Auto.auto_tac ~dbd ~params
-              ~automation_cache:grafite_status.GrafiteTypes.automation_cache) 
+              ~automation_cache:grafite_status#automation_cache) 
             proof_status
         in
         let proof_term = 
@@ -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 
@@ -802,7 +801,7 @@ object (self)
    buffer#insert ~iter:(buffer#get_iter_at_mark (`MARK locked_mark)) newtext;
    (* here we need to set the Goal in case we are going to cursor (or to
       bottom) and we will face a macro *)
-   match self#grafite_status.proof_status with
+   match self#grafite_status#proof_status with
       Incomplete_proof p ->
        userGoal <-
          (try Some (Continuationals.Stack.find_goal p.stack)
@@ -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 <- [];
@@ -1094,7 +1089,7 @@ object (self)
      HLog.error "The script is too big!\n"
   
   method onGoingProof () =
-    match self#grafite_status.proof_status with
+    match self#grafite_status#proof_status with
     | No_proof | Proof _ -> false
     | Incomplete_proof _ -> true
     | Intermediate _ -> assert false
@@ -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 _