From 779859f7a9e317e378d258897c289f447adea7ad Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 19 Jun 2009 10:16:23 +0000 Subject: [PATCH] Estatus finally merged into the global status using inheritance. Major code simplification everywhere :-) --- .../grafite_engine/grafiteEngine.ml | 187 ++++++++---------- .../components/grafite_engine/grafiteSync.ml | 11 +- .../components/grafite_engine/grafiteTypes.ml | 45 ++--- .../grafite_engine/grafiteTypes.mli | 18 +- helm/software/matita/matita.ml | 12 +- helm/software/matita/matitaEngine.ml | 90 ++++----- helm/software/matita/matitaGui.ml | 4 +- helm/software/matita/matitaGuiTypes.mli | 2 +- helm/software/matita/matitaMathView.ml | 7 +- helm/software/matita/matitaScript.ml | 19 +- helm/software/matita/matitaWiki.ml | 6 +- helm/software/matita/matitacLib.ml | 7 +- 12 files changed, 162 insertions(+), 246 deletions(-) diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 192e396af..5f64b1b0a 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -482,17 +482,13 @@ let inject_unification_hint = ;; let eval_unification_hint status t n = - let estatus = GrafiteTypes.get_estatus status in - let metasenv,subst,estatus,t = - GrafiteDisambiguate.disambiguate_nterm None estatus [] [] [] ("",0,t) in + let metasenv,subst,status,t = + GrafiteDisambiguate.disambiguate_nterm None status [] [] [] ("",0,t) in assert (metasenv=[]); let t = NCicUntrusted.apply_subst subst [] t in - let status = GrafiteTypes.set_estatus estatus status in - let estatus = - basic_eval_unification_hint (t,n) (GrafiteTypes.get_estatus status) in - let dump = inject_unification_hint (t,n)::estatus#dump in - let estatus = estatus#set_dump dump in - let status = GrafiteTypes.set_estatus estatus status in + let status = basic_eval_unification_hint (t,n) status in + let dump = inject_unification_hint (t,n)::status#dump in + let status = status#set_dump dump in status,`Old [] ;; @@ -659,84 +655,79 @@ let rec eval_ng_tac (text, prefix_len, tac) = | GrafiteAst.NAssumption _ -> NTactics.assumption_tac ;; -let subst_metasenv_and_fix_names s = - let u,h,metasenv, subst,o = s#obj in +let subst_metasenv_and_fix_names status = + let u,h,metasenv, subst,o = status#obj in let o = NCicUntrusted.map_obj_kind ~skip_body:true (NCicUntrusted.apply_subst subst []) o in - s#set_obj (u,h,NCicUntrusted.apply_subst_metasenv subst metasenv,subst,o) + status#set_obj(u,h,NCicUntrusted.apply_subst_metasenv subst metasenv,subst,o) ;; let rec eval_ncommand opts status (text,prefix_len,cmd) = match cmd with | GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n | GrafiteAst.NQed loc -> - (match status#ng_status with - | GrafiteTypes.ProofMode estatus -> - let uri,height,menv,subst,obj_kind = estatus#obj in - if menv <> [] then - raise - (GrafiteTypes.Command_error"You can't Qed an incomplete theorem") - else - let obj_kind = - NCicUntrusted.map_obj_kind - (NCicUntrusted.apply_subst subst []) obj_kind in - let height = NCicTypeChecker.height_of_obj_kind uri obj_kind in - (* fix the height inside the object *) - let rec fix () = function - | NCic.Const (NReference.Ref (u,spec)) when NUri.eq u uri -> - NCic.Const (NReference.reference_of_spec u - (match spec with - | NReference.Def _ -> NReference.Def height - | NReference.Fix (i,j,_) -> NReference.Fix(i,j,height) - | NReference.CoFix _ -> NReference.CoFix height - | NReference.Ind _ | NReference.Con _ - | NReference.Decl as s -> s)) - | t -> NCicUtils.map (fun _ () -> ()) () fix t - in - let obj_kind = - match obj_kind with - | NCic.Fixpoint _ -> - NCicUntrusted.map_obj_kind (fix ()) obj_kind - | _ -> obj_kind - in - let obj = uri,height,[],[],obj_kind in - NCicTypeChecker.typecheck_obj obj; - let estatus = NCicLibrary.add_obj estatus uri obj in - let objs = NCicElim.mk_elims obj in - let timestamp,uris_rev = - List.fold_left - (fun (estatus,uris_rev) (uri,_,_,_,_) as obj -> - NCicTypeChecker.typecheck_obj obj; - let estatus = NCicLibrary.add_obj estatus uri obj in - estatus,uri::uris_rev - ) (estatus,[]) objs in - let uris = uri::List.rev uris_rev in - status#set_ng_status - (GrafiteTypes.CommandMode (estatus :> NEstatus.status)),`New uris - | _ -> raise (GrafiteTypes.Command_error "Not in proof mode")) + if status#ng_mode <> `ProofMode then + raise (GrafiteTypes.Command_error "Not in proof mode") + else + let uri,height,menv,subst,obj_kind = status#obj in + if menv <> [] then + raise + (GrafiteTypes.Command_error"You can't Qed an incomplete theorem") + else + let obj_kind = + NCicUntrusted.map_obj_kind + (NCicUntrusted.apply_subst subst []) obj_kind in + let height = NCicTypeChecker.height_of_obj_kind uri obj_kind in + (* fix the height inside the object *) + let rec fix () = function + | NCic.Const (NReference.Ref (u,spec)) when NUri.eq u uri -> + NCic.Const (NReference.reference_of_spec u + (match spec with + | NReference.Def _ -> NReference.Def height + | NReference.Fix (i,j,_) -> NReference.Fix(i,j,height) + | NReference.CoFix _ -> NReference.CoFix height + | NReference.Ind _ | NReference.Con _ + | NReference.Decl as s -> s)) + | t -> NCicUtils.map (fun _ () -> ()) () fix t + in + let obj_kind = + match obj_kind with + | NCic.Fixpoint _ -> + NCicUntrusted.map_obj_kind (fix ()) obj_kind + | _ -> obj_kind + in + let obj = uri,height,[],[],obj_kind in + NCicTypeChecker.typecheck_obj obj; + let status = NCicLibrary.add_obj status uri obj in + let objs = NCicElim.mk_elims obj in + let timestamp,uris_rev = + List.fold_left + (fun (status,uris_rev) (uri,_,_,_,_) as obj -> + NCicTypeChecker.typecheck_obj obj; + let status = NCicLibrary.add_obj status uri obj in + status,uri::uris_rev + ) (status,[]) objs in + let uris = uri::List.rev uris_rev in + status#set_ng_mode `CommandMode,`New uris | GrafiteAst.NObj (loc,obj) -> - let estatus = - match status#ng_status with - | GrafiteTypes.ProofMode _ -> assert false - | GrafiteTypes.CommandMode es -> es - in - let estatus,obj = - GrafiteDisambiguate.disambiguate_nobj estatus - ~baseuri:status#baseuri (text,prefix_len,obj) in - let uri,height,nmenv,nsubst,nobj = obj in - let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in - let status = - status#set_ng_status - (GrafiteTypes.ProofMode - (subst_metasenv_and_fix_names - ((new NTacStatus.status obj ninitial_stack)#set_estatus estatus))) - in - (match nmenv with - [] -> - eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc) - | _ -> status,`New []) + if status#ng_mode <> `CommandMode then + raise (GrafiteTypes.Command_error "Not in command mode") + else + let status,obj = + GrafiteDisambiguate.disambiguate_nobj status + ~baseuri:status#baseuri (text,prefix_len,obj) in + let uri,height,nmenv,nsubst,nobj = obj in + let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in + let status = status#set_obj obj in + let status = status#set_stack ninitial_stack in + let status = subst_metasenv_and_fix_names status in + let status = status#set_ng_mode `ProofMode in + (match nmenv with + [] -> + eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc) + | _ -> status,`New []) | GrafiteAst.NUnivConstraint (loc,strict,u1,u2) -> NCicEnvironment.add_constraint strict [false,u1] [false,u2]; status, `New [u1;u2] @@ -819,26 +810,11 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status raise (IncludedFileNotCompiled (moopath_rw,baseuri)) in let status = eval_from_moo.efm_go status moopath in - let estatus = GrafiteTypes.get_estatus status in - let estatus = + let status = NRstatus.Serializer.require ~baseuri:(NUri.uri_of_string baseuri) - estatus in - let status = GrafiteTypes.set_estatus estatus status in -(* debug - let lt_uri = UriManager.uri_of_string "cic:/matita/nat/orders/lt.con" in - let nat_uri = UriManager.uri_of_string "cic:/matita/nat/nat/nat.ind" in - let nat = Cic.MutInd(nat_uri,0,[]) in - let zero = Cic.MutConstruct(nat_uri,0,1,[]) in - let succ = Cic.MutConstruct(nat_uri,0,2,[]) in - let fake= Cic.Meta(-1,[]) in - let term= Cic.Appl [Cic.Const (lt_uri,[]);zero;Cic.Appl[succ;zero]] in let msg = - let candidates = Universe.get_candidates status.GrafiteTypes.universe term in - ("candidates for " ^ (CicPp.ppterm term) ^ " = " ^ - (String.concat "\n" (List.map CicPp.ppterm candidates))) + status in - prerr_endline msg; -*) - status,`Old [] + status,`Old [] | GrafiteAst.Print (_,"proofterm") -> let _,_,_,p,_, _ = GrafiteTypes.get_current_proof status in prerr_endline (Auto.pp_proofterm (Lazy.force p)); @@ -961,18 +937,17 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status eval_tactical status (punctuation_tactical_of_ast (text,prefix_len,punct)),`Old [] | GrafiteAst.NTactic (_(*loc*), tacl) -> - (match status#ng_status with - | GrafiteTypes.CommandMode _ -> assert false - | GrafiteTypes.ProofMode nstatus -> - let nstatus = - List.fold_left - (fun nstatus tac -> - let nstatus = eval_ng_tac (text,prefix_len,tac) nstatus in - subst_metasenv_and_fix_names nstatus) - nstatus tacl - in - status#set_ng_status (GrafiteTypes.ProofMode nstatus), - `New []) + if status#ng_mode <> `ProofMode then + raise (GrafiteTypes.Command_error "Not in proof mode") + else + let status = + List.fold_left + (fun status tac -> + let status = eval_ng_tac (text,prefix_len,tac) status in + subst_metasenv_and_fix_names status) + status tacl + in + status,`New [] | GrafiteAst.NonPunctuationTactical (_, tac, punct) -> let status = eval_tactical status diff --git a/helm/software/components/grafite_engine/grafiteSync.ml b/helm/software/components/grafite_engine/grafiteSync.ml index 5cf9dc360..ca29d39fc 100644 --- a/helm/software/components/grafite_engine/grafiteSync.ml +++ b/helm/software/components/grafite_engine/grafiteSync.ml @@ -147,10 +147,7 @@ let add_coercion ~pack_coercion_obj ~add_composites status uri arity #set_coercions (CoercDb.dump ())) ; #set_objects (lemmas @ status#objects) in - let estatus = - NCicCoercion.index_old_db (CoercDb.dump ()) (GrafiteTypes.get_estatus status) - in - let status = GrafiteTypes.set_estatus estatus status in + let status = NCicCoercion.index_old_db (CoercDb.dump ()) status in status, lemmas let prefer_coercion status u = @@ -170,13 +167,11 @@ let time_travel ~present ~past = uri_list_diff present#objects past#objects in List.iter LibrarySync.remove_obj objs_to_remove; CoercDb.restore past#coercions; - NCicLibrary.time_travel (GrafiteTypes.get_estatus past) + NCicLibrary.time_travel past ;; let initial_status lexicon_status baseuri = - new GrafiteTypes.status [] GrafiteTypes.No_proof [] - CoercDb.empty_coerc_db (AutomationCache.empty ()) - baseuri (GrafiteTypes.CommandMode (new NEstatus.status)) + (new GrafiteTypes.status baseuri)#set_lstatus lexicon_status#lstatus ;; let init baseuri = diff --git a/helm/software/components/grafite_engine/grafiteTypes.ml b/helm/software/components/grafite_engine/grafiteTypes.ml index 959d96f36..96ae9acfd 100644 --- a/helm/software/components/grafite_engine/grafiteTypes.ml +++ b/helm/software/components/grafite_engine/grafiteTypes.ml @@ -44,23 +44,19 @@ type proof_status = (* Status in which the proof could be while it is being processed by the * engine. No status entering/exiting the engine could be in it. *) -type ng_status = - | ProofMode of NTacStatus.tac_status - | CommandMode of NEstatus.status - -class status = - fun (mcr : GrafiteMarshal.moo) (ps : proof_status) (o : UriManager.uri list) - (c : CoercDb.coerc_db) (ac : AutomationCache.cache) (b : string) - (ns : ng_status) - -> +class status = fun (b : string) -> + let fake_obj = + NUri.uri_of_string "cic:/matita/dummy.decl",0,[],[], + NCic.Constant([],"",None,NCic.Implicit `Closed,(`Provided,`Theorem,`Regular)) + in object - val moo_content_rev = mcr - val proof_status = ps - val objects = o - val coercions = c - val automation_cache = ac + val moo_content_rev = ([] : GrafiteMarshal.moo) + val proof_status = No_proof + val objects = ([] : UriManager.uri list) + val coercions = CoercDb.empty_coerc_db + val automation_cache = AutomationCache.empty () val baseuri = b - val ng_status = ns + val ng_mode = (`CommandMode : [`CommandMode | `ProofMode]) method moo_content_rev = moo_content_rev method set_moo_content_rev v = {< moo_content_rev = v >} method proof_status = proof_status @@ -73,23 +69,12 @@ class status = method set_automation_cache v = {< automation_cache = v >} method baseuri = baseuri method set_baseuri v = {< baseuri = v >} - method ng_status = ng_status; - method set_ng_status v = {< ng_status = v >} + method ng_mode = ng_mode; + method set_ng_mode v = {< ng_mode = v >} + (* Warning: #stack and #obj are meaningful iff #ng_mode is `ProofMode *) + inherit ([Continuationals.Stack.t] NTacStatus.status fake_obj (Continuationals.Stack.empty)) end -let get_estatus x = - match x#ng_status with - | ProofMode t -> (t :> NEstatus.status) - | CommandMode e -> e -;; - -let set_estatus e x = - x#set_ng_status - (match x#ng_status with - ProofMode t -> ProofMode t#set_estatus e - | CommandMode _ -> CommandMode e) -;; - let get_current_proof status = match status#proof_status with | Incomplete_proof { proof = p } -> p diff --git a/helm/software/components/grafite_engine/grafiteTypes.mli b/helm/software/components/grafite_engine/grafiteTypes.mli index 34e3d0966..4e2decc9c 100644 --- a/helm/software/components/grafite_engine/grafiteTypes.mli +++ b/helm/software/components/grafite_engine/grafiteTypes.mli @@ -42,18 +42,8 @@ type proof_status = | Proof of ProofEngineTypes.proof | Intermediate of Cic.metasenv -type ng_status = - | ProofMode of NTacStatus.tac_status - | CommandMode of NEstatus.status - class status : - GrafiteMarshal.moo -> - proof_status -> - UriManager.uri list -> - CoercDb.coerc_db -> - AutomationCache.cache -> string -> - ng_status -> object ('self) method moo_content_rev: GrafiteMarshal.moo method set_moo_content_rev: GrafiteMarshal.moo -> 'self @@ -67,8 +57,10 @@ class status : method set_automation_cache:AutomationCache.cache -> 'self method baseuri: string method set_baseuri: string -> 'self - method ng_status: ng_status - method set_ng_status: ng_status -> 'self + method ng_mode: [`ProofMode | `CommandMode] + method set_ng_mode: [`ProofMode | `CommandMode] -> 'self + (* Warning: #stack and #obj are meaningful iff #ng_mode is `ProofMode *) + inherit NTacStatus.tac_status end val dump_status : status -> unit @@ -81,8 +73,6 @@ val get_proof_metasenv: status -> Cic.metasenv val get_stack: status -> Continuationals.Stack.t val get_proof_context : status -> int -> Cic.context val get_proof_conclusion : status -> int -> Cic.term -val get_estatus : status -> NEstatus.status val set_stack: Continuationals.Stack.t -> status -> status val set_metasenv: Cic.metasenv -> status -> status -val set_estatus : NEstatus.status -> status -> status diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml index 1b4cc5a3c..cd3fe7982 100644 --- a/helm/software/matita/matita.ml +++ b/helm/software/matita/matita.ml @@ -107,12 +107,12 @@ let _ = with Failure _ -> script#setGoal None); | Proof proof -> sequents_viewer#load_logo_with_qed | No_proof -> - (match grafite_status#ng_status with - ProofMode nstatus -> - sequents_viewer#nload_sequents nstatus; + (match grafite_status#ng_mode with + `ProofMode -> + sequents_viewer#nload_sequents grafite_status; (try script#setGoal - (Some (Continuationals.Stack.find_goal nstatus#stack)); + (Some (Continuationals.Stack.find_goal grafite_status#stack)); let goal = match script#goal with None -> assert false @@ -120,7 +120,7 @@ let _ = in sequents_viewer#goto_sequent goal with Failure _ -> script#setGoal None); - | CommandMode _ -> sequents_viewer#load_logo + | `CommandMode -> sequents_viewer#load_logo ) | Intermediate _ -> assert false (* only the engine may be in this state *) in @@ -141,7 +141,7 @@ let _ = ignore (GMenu.separator_item ~packing:gui#main#debugMenu_menu#append ()) in addDebugItem "dump aliases" (fun _ -> - let status = GrafiteTypes.get_estatus script#grafite_status in + let status = script#grafite_status in LexiconEngine.dump_aliases HLog.debug "" status); (* FG: DEBUGGING addDebugItem "dump interpretations" (fun _ -> diff --git a/helm/software/matita/matitaEngine.ml b/helm/software/matita/matitaEngine.ml index ba4e34696..a2effbe03 100644 --- a/helm/software/matita/matitaEngine.ml +++ b/helm/software/matita/matitaEngine.ml @@ -58,43 +58,38 @@ let disambiguate_macro lexicon_status_ref grafite_status macro context = in GrafiteTypes.set_metasenv metasenv grafite_status,macro -let eval_ast ?do_heavy_checks grafite_status (text,prefix_len,ast) = - let lexicon_status = GrafiteTypes.get_estatus grafite_status in +let eval_ast ?do_heavy_checks status (text,prefix_len,ast) = let dump = not (Helm_registry.get_bool "matita.moo") in - let lexicon_status_ref = ref (lexicon_status :> LexiconEngine.status) in - let baseuri = grafite_status#baseuri in - let new_grafite_status,new_objs = + let lexicon_status_ref = ref (status :> LexiconEngine.status) in + let baseuri = status#baseuri in + let new_status,new_objs = match ast with | G.Executable (_, G.Command (_, G.Coercion _)) when dump -> (* FG: some commands can not be executed when mmas are parsed *************) (* To be removed when mmas will be executed *) - grafite_status, `Old [] + status, `Old [] | ast -> GrafiteEngine.eval_ast ~disambiguate_tactic:(disambiguate_tactic text prefix_len lexicon_status_ref) ~disambiguate_command:(disambiguate_command lexicon_status_ref) ~disambiguate_macro:(disambiguate_macro lexicon_status_ref) - ?do_heavy_checks grafite_status (text,prefix_len,ast) + ?do_heavy_checks status (text,prefix_len,ast) in - let new_lexicon_status = GrafiteTypes.get_estatus new_grafite_status in - let new_lexicon_status = - if !lexicon_status_ref#lstatus != lexicon_status#lstatus then - new_lexicon_status#set_lstatus (!lexicon_status_ref#lstatus) + let new_status = + if !lexicon_status_ref#lstatus != status#lstatus then + new_status#set_lstatus (!lexicon_status_ref#lstatus) else - new_lexicon_status in - let new_lexicon_status = - LexiconSync.add_aliases_for_objs new_lexicon_status new_objs in - let new_aliases = - LexiconSync.alias_diff ~from:lexicon_status new_lexicon_status in + new_status in + let new_status = LexiconSync.add_aliases_for_objs new_status new_objs in + let new_aliases = LexiconSync.alias_diff ~from:status new_status in let _,intermediate_states = List.fold_left - (fun (lexicon_status,acc) (k,value) -> + (fun (status,acc) (k,value) -> let v = LexiconAst.description_of_alias value in let b = try (* this hack really sucks! *) - UriManager.buri_of_uri (UriManager.uri_of_string v) = - baseuri + UriManager.buri_of_uri (UriManager.uri_of_string v) = baseuri with UriManager.IllFormedUri _ -> try @@ -107,21 +102,15 @@ let eval_ast ?do_heavy_checks grafite_status (text,prefix_len,ast) = false (* v is a description, not a URI *) in if b then - lexicon_status,acc + status,acc else - let new_lexicon_status = - LexiconEngine.set_proof_aliases lexicon_status [k,value] - in - let grafite_status = - GrafiteTypes.set_estatus new_lexicon_status grafite_status + let new_status = + LexiconEngine.set_proof_aliases status [k,value] in - new_lexicon_status, (grafite_status ,Some (k,value))::acc - ) (lexicon_status,[]) new_aliases - in - let new_grafite_status = - GrafiteTypes.set_estatus new_lexicon_status new_grafite_status + new_status, (new_status ,Some (k,value))::acc + ) (status,[]) new_aliases in - ((new_grafite_status),None)::intermediate_states + ((new_status),None)::intermediate_states ;; exception TryingToAdd of string @@ -129,10 +118,10 @@ exception EnrichedWithStatus of exn * GrafiteTypes.status let eval_from_stream ~first_statement_only ~include_paths ?do_heavy_checks ?(enforce_no_new_aliases=true) - ?(watch_statuses=fun _ -> ()) grafite_status str cb + ?(watch_statuses=fun _ -> ()) status str cb = let matita_debug = Helm_registry.get_bool "matita.debug" in - let rec loop grafite_status statuses = + let rec loop status statuses = let loop = if first_statement_only then fun _ statuses -> statuses else loop @@ -140,27 +129,18 @@ let eval_from_stream ~first_statement_only ~include_paths let stop,g,s = try let cont = - try - let lexicon_status = GrafiteTypes.get_estatus grafite_status in - Some (GrafiteParser.parse_statement ~include_paths str lexicon_status) - with - End_of_file -> None - in + try Some (GrafiteParser.parse_statement ~include_paths str status) + with End_of_file -> None in match cont with - | None -> true, grafite_status, statuses - | Some (lexicon_status,ast) -> - let grafite_status = - GrafiteTypes.set_estatus lexicon_status grafite_status - in + | None -> true, status, statuses + | Some (status,ast) -> (match ast with GrafiteParser.LNone _ -> - watch_statuses grafite_status ; - false, grafite_status, - (((grafite_status),None)::statuses) + watch_statuses status ; + false, status, ((status,None)::statuses) | GrafiteParser.LSome ast -> - cb grafite_status ast; - let new_statuses = - eval_ast ?do_heavy_checks grafite_status ("",0,ast) in + cb status ast; + let new_statuses = eval_ast ?do_heavy_checks status ("",0,ast) in if enforce_no_new_aliases then List.iter (fun (_,alias) -> @@ -169,17 +149,17 @@ let eval_from_stream ~first_statement_only ~include_paths | Some (k,value) -> let newtxt = LexiconAstPp.pp_alias value in raise (TryingToAdd newtxt)) new_statuses; - let grafite_status = + let status = match new_statuses with [] -> assert false | (s,_)::_ -> s in - watch_statuses grafite_status ; - false, grafite_status, (new_statuses @ statuses)) + watch_statuses status ; + false, status, (new_statuses @ statuses)) with exn when not matita_debug -> - raise (EnrichedWithStatus (exn, grafite_status)) + raise (EnrichedWithStatus (exn, status)) in if stop then s else loop g s in - loop grafite_status [] + loop status [] ;; diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index 5272f07a7..8b38950bb 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -87,9 +87,9 @@ let save_moo grafite_status = in GrafiteMarshal.save_moo moo_fname grafite_status#moo_content_rev; LexiconMarshal.save_lexicon lexicon_fname - (GrafiteTypes.get_estatus grafite_status)#lstatus.LexiconEngine.lexicon_content_rev; + grafite_status#lstatus.LexiconEngine.lexicon_content_rev; NRstatus.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) - (GrafiteTypes.get_estatus grafite_status)#dump + grafite_status#dump | _ -> clean_current_baseuri grafite_status ;; diff --git a/helm/software/matita/matitaGuiTypes.mli b/helm/software/matita/matitaGuiTypes.mli index 18515dac5..fb8c1f14a 100644 --- a/helm/software/matita/matitaGuiTypes.mli +++ b/helm/software/matita/matitaGuiTypes.mli @@ -136,7 +136,7 @@ object method load_logo: unit method load_logo_with_qed: unit method load_sequents: GrafiteTypes.incomplete_proof -> unit - method nload_sequents: NTacStatus.tac_status -> unit + method nload_sequents: #NTacStatus.tac_status -> unit method goto_sequent: int -> unit (* to be called _after_ load_sequents *) method cicMathView: cicMathView diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml index 22ad1e4cf..f00ea1a0f 100644 --- a/helm/software/matita/matitaMathView.ml +++ b/helm/software/matita/matitaMathView.ml @@ -798,7 +798,8 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = self#script#setGoal (Some (goal_of_switch goal_switch)); self#render_page ~page ~goal_switch)) - method nload_sequents (status : NTacStatus.tac_status) = + method nload_sequents : 'status. #NTacStatus.tac_status as 'status -> unit + = fun status -> let _,_,metasenv,subst,_ = status#obj in _metasenv <- `New (metasenv,subst); pages <- 0; @@ -1348,8 +1349,8 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) in self#_loadObj obj | _ -> - match self#script#grafite_status#ng_status with - ProofMode tstatus -> self#_loadNObj tstatus#obj + match self#script#grafite_status#ng_mode with + `ProofMode -> self#_loadNObj self#script#grafite_status#obj | _ -> self#blank () (** loads a cic uri from the environment diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index 108b23237..e72644d10 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -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 @@ -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 <- []; @@ -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 _ diff --git a/helm/software/matita/matitaWiki.ml b/helm/software/matita/matitaWiki.ml index 30c7fc9ea..f9c9af359 100644 --- a/helm/software/matita/matitaWiki.ml +++ b/helm/software/matita/matitaWiki.ml @@ -141,8 +141,7 @@ let rec interactive_loop () = grafite_status := drop (to_be_dropped, !grafite_status) ; let grafite_status = safe_hd !grafite_status in LexiconSync.time_travel - ~present:(GrafiteTypes.get_estatus cur_grafite_status) - ~past:(GrafiteTypes.get_estatus grafite_status); + ~present:cur_grafite_status ~past:grafite_status; GrafiteSync.time_travel ~present:cur_grafite_status ~past:grafite_status; interactive_loop (Some n) @@ -226,8 +225,7 @@ let main () = match !grafite_status with | s::_ -> s#proof_status, s#moo_content_rev, - (GrafiteTypes.get_estatus s)#lstatus.LexiconEngine.lexicon_content_rev, - (GrafiteTypes.get_estatus s)#dump + s#lstatus.LexiconEngine.lexicon_content_rev, s#dump | _ -> assert false in if proof_status <> GrafiteTypes.No_proof then diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml index 18b406708..36f7cda6d 100644 --- a/helm/software/matita/matitacLib.ml +++ b/helm/software/matita/matitacLib.ml @@ -235,8 +235,7 @@ let compile atstart options fname = with | [] -> grafite_status | (g,None)::_ -> g - | (g,Some _)::_ -> - raise (AttemptToInsertAnAlias (GrafiteTypes.get_estatus g)) + | (g,Some _)::_ -> raise (AttemptToInsertAnAlias g) with MatitaEngine.EnrichedWithStatus (GrafiteEngine.Macro (floc, f), grafite) as exn -> match f (get_macro_context (Some grafite)) with @@ -258,7 +257,7 @@ let compile atstart options fname = let elapsed = Unix.time () -. time in let proof_status,moo_content_rev,lexicon_content_rev = grafite_status#proof_status, grafite_status#moo_content_rev, - (GrafiteTypes.get_estatus grafite_status)#lstatus.LexiconEngine.lexicon_content_rev + grafite_status#lstatus.LexiconEngine.lexicon_content_rev in if proof_status <> GrafiteTypes.No_proof then (HLog.error @@ -275,7 +274,7 @@ let compile atstart options fname = GrafiteMarshal.save_moo moo_fname moo_content_rev; LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev; NRstatus.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) - (GrafiteTypes.get_estatus grafite_status)#dump + grafite_status#dump end; let tm = Unix.gmtime elapsed in let sec = string_of_int tm.Unix.tm_sec ^ "''" in -- 2.39.2