huge commit regarding the grafite_status:

[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 66da43c8f36259edc8111f14014a658a42755f4b..2ee136dfe753e56dbf7dd3781432ad7a72fc769b 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteTypes.ml
+++ b/helm/software/components/grafite_engine/grafiteTypes.ml
@@ -46,7 +46,7 @@ type proof_status =
 
 type ng_status =
   | ProofMode of NTacStatus.tac_status
-  | CommandMode of LexiconEngine.status
+  | CommandMode of NEstatus.extra_status
 
 type status = {
   moo_content_rev: GrafiteMarshal.moo;
@@ -58,6 +58,48 @@ type status = {
   ng_status: ng_status;
 }
 
+let get_lexicon x = 
+  match x.ng_status with
+  | ProofMode t -> t.NTacStatus.istatus.NTacStatus.estatus.NEstatus.lstatus
+  | CommandMode e -> e.NEstatus.lstatus
+;;
+ 
+let set_lexicon new_lexicon_status new_grafite_status = 
+  { new_grafite_status with ng_status =
+   match new_grafite_status.ng_status with
+   | CommandMode estatus -> 
+      CommandMode 
+        { estatus with NEstatus.lstatus = new_lexicon_status }
+   | ProofMode t -> 
+       ProofMode 
+        { t with NTacStatus.istatus = 
+          { t.NTacStatus.istatus with NTacStatus.estatus = 
+            { t.NTacStatus.istatus.NTacStatus.estatus with NEstatus.lstatus =
+               new_lexicon_status }}}}
+;; 
+
+let set_coercions db new_grafite_status = 
+  { new_grafite_status with ng_status =
+   match new_grafite_status.ng_status with
+   | CommandMode estatus -> 
+      CommandMode 
+        { estatus with NEstatus.rstatus = 
+          { estatus.NEstatus.rstatus with NRstatus.coerc_db = db }}
+   | ProofMode t -> 
+       ProofMode 
+        { t with NTacStatus.istatus = 
+          { t.NTacStatus.istatus with NTacStatus.estatus = 
+            { t.NTacStatus.istatus.NTacStatus.estatus with NEstatus.rstatus =
+              { t.NTacStatus.istatus.NTacStatus.estatus.NEstatus.rstatus with NRstatus.coerc_db = db
+        }}}}}
+;; 
+
+let get_estatus x = 
+  match x.ng_status with
+  | ProofMode t -> t.NTacStatus.istatus.NTacStatus.estatus
+  | CommandMode e -> e
+;;
+
 let get_current_proof status =
   match status.proof_status with
   | Incomplete_proof { proof = p } -> p
@@ -191,3 +233,8 @@ let dump_status status =
   List.iter 
     (fun u -> HLog.message (UriManager.string_of_uri u)) status.objects 
   
+let get_coercions new_grafite_status = 
+   let e = get_estatus new_grafite_status in
+   e.NEstatus.rstatus.NRstatus.coerc_db 
+;;
+