Estatus finally merged into the global status using inheritance.

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

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index 05dad0572be58cdc72bb1b650b7be81c3e8c6fe4..e72644d105a6f238703539c4edc7c8c3847a4265 100644 (file)
--- 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
@@ -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_lexicon grafite_status)
+            grafite_status
         in
           ast, text
-    | `Ast (st, text) -> (GrafiteTypes.get_lexicon grafite_status, st), text
+    | `Ast (st, text) -> (grafite_status, st), text
   in
-  let grafite_status = GrafiteTypes.set_lexicon 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 +674,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
@@ -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_lexicon cur_grafite_status)
-      ~past:(GrafiteTypes.get_lexicon 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_lexicon self#grafite_status)
-      ~past:(GrafiteTypes.get_lexicon 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_lexicon self#grafite_status) self#getFuture
+    try is_there_only_comments self#grafite_status self#getFuture
     with 
     | LexiconEngine.IncludedFileNotCompiled _
     | HExtlib.Localized _