freescale porting, work in progress

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

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index 8de5ccebc3dd74f54d218b85ccdf065b7e5ddf77..bbe76859f3daf7f1ffffaba61175940114e47f85 100644 (file)
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -74,8 +74,6 @@ type guistuff = {
 let eval_with_engine include_paths guistuff grafite_status user_goal
  skipped_txt nonskipped_txt st
 =
-  let module TAPp = GrafiteAstPp in
-  let module DTE = DisambiguateTypes.Environment in
   let parsed_text_length =
     String.length skipped_txt + String.length nonskipped_txt 
   in
@@ -212,7 +210,7 @@ let cic2grafite context menv t =
       | Cic.Const _ as t -> 
           PT.Ident (pp_t c t, None)
       | Cic.Appl l -> PT.Appl (List.map (aux c) l)
-      | Cic.Implicit _ -> PT.Implicit
+      | Cic.Implicit _ -> PT.Implicit `JustOne
       | Cic.Lambda (Cic.Name n, s, t) ->
           PT.Binder (`Lambda, (PT.Ident (n,None), Some (aux c s)),
             aux (Some (Cic.Name n, Cic.Decl s)::c) t)
@@ -222,7 +220,7 @@ let cic2grafite context menv t =
       | Cic.LetIn (Cic.Name n, s, ty, t) ->
           PT.Binder (`Lambda, (PT.Ident (n,None), Some (aux c s)),
             aux (Some (Cic.Name n, Cic.Def (s,ty))::c) t)
-      | Cic.Meta _ -> PT.Implicit
+      | Cic.Meta _ -> PT.Implicit `JustOne
       | Cic.Sort (Cic.Type u) -> PT.Sort (`Type u)
       | Cic.Sort Cic.Set -> PT.Sort `Set
       | Cic.Sort (Cic.CProp u) -> PT.Sort (`CProp u)
@@ -369,11 +367,8 @@ let cic2grafite context menv t =
 ;;
 
 let rec eval_macro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac =
-  let module TAPp = GrafiteAstPp in
   let module MQ = MetadataQuery in
-  let module MDB = LibraryDb in
   let module CTC = CicTypeChecker in
-  let module CU = CicUniv in
   (* no idea why ocaml wants this *)
   let parsed_text_length = String.length parsed_text in
   let dbd = LibraryDb.instance () in
@@ -485,7 +480,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 +507,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 = 
@@ -581,9 +576,6 @@ and eval_executable include_paths (buffer : GText.buffer) guistuff
 grafite_status user_goal unparsed_text skipped_txt nonskipped_txt
 script ex loc
 =
- let module TAPp = GrafiteAstPp in
- let module MD = MultiPassDisambiguator in
- let module ML = MatitaMisc in
   try
    ignore (buffer#move_mark (`NAME "beginning_of_statement")
     ~where:((buffer#get_iter_at_mark (`NAME "locked"))#forward_chars
@@ -605,19 +597,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 +793,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 +806,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 +973,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 +1081,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 +1127,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 _