;;
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 []
;;
| 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]
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));
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
#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 =
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 =
(* 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
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
| 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
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
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
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
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
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 _ ->
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
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
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
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) ->
| 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 []
;;
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
;;
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
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;
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
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
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;
(* 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 <- [];
| 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 _
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)
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
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
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
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
projects / helm.git / commitdiff