Estatus finally merged into the global status using inheritance.

[helm.git] / helm / software / components / grafite_engine / grafiteTypes.mli

diff --git a/helm/software/components/grafite_engine/grafiteTypes.mli b/helm/software/components/grafite_engine/grafiteTypes.mli
index 34e3d09660c0b2e8c7a809d324bdd46a006d7d3d..4e2decc9c863498fc442271223774cf7ede2257d 100644 (file)
--- 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