(* 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