Estatus finally merged into the global status using inheritance.

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

diff --git a/helm/software/components/grafite_engine/grafiteTypes.ml b/helm/software/components/grafite_engine/grafiteTypes.ml
index 959d96f368b4694ce69d9fe97db907eba6ab04f4..96ae9acfd0aebe334432140ef9dae4e7925326ad 100644 (file)
--- 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