X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteTypes.mli;h=4e2decc9c863498fc442271223774cf7ede2257d;hb=e9b09b14538f770b9e65083c24e3e9cf487df648;hp=c30beead02301170bf77e08cb3ea9dbcf5183867;hpb=290350836dd1727b3e3cdd4ee71e666a39cc4a09;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteTypes.mli b/helm/software/components/grafite_engine/grafiteTypes.mli
index c30beead0..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
@@ -76,15 +68,11 @@ val dump_status : status -> unit
   (** list is not reversed, head command will be the first emitted *)
 val add_moo_content: GrafiteMarshal.ast_command list -> status -> status
 
-val get_baseuri: status -> string 
-
 val get_current_proof: status -> ProofEngineTypes.proof
 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