More statuses converted to objects.

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

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index 8de5ccebc3dd74f54d218b85ccdf065b7e5ddf77..108b23237d74e9db01195ffb456a73bbba80b1df 100644 (file)
--- 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 = 
@@ -802,7 +802,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)
@@ -1094,7 +1094,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