X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteTypes.ml;h=96ae9acfd0aebe334432140ef9dae4e7925326ad;hb=62ab884c6ce7dd41c6e6fa2efc5102b23f57de32;hp=9fd40b1c463af8c80b80002c4703b81cdbe1c8c8;hpb=290350836dd1727b3e3cdd4ee71e666a39cc4a09;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteTypes.ml b/helm/software/components/grafite_engine/grafiteTypes.ml
index 9fd40b1c4..96ae9acfd 100644
--- 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
@@ -166,8 +151,6 @@ let add_moo_content cmds status =
     GrafiteAstPp.pp_command content')); *)
    status#set_moo_content_rev content'
 
-let get_baseuri status = status#baseuri;;
-
 let dump_status status = 
   HLog.message "status.aliases:\n";
   HLog.message "status.proof_status:";