X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaScript.ml;h=bbe76859f3daf7f1ffffaba61175940114e47f85;hb=20166e1ce9d14f6a3586a10d98ac3f1571207586;hp=8de5ccebc3dd74f54d218b85ccdf065b7e5ddf77;hpb=df1201e37d6f2631dc31ffc87b979a6c81180a3a;p=helm.git diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index 8de5ccebc..bbe76859f 100644 --- 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 _