EXPERIMENTAL COMMIT (by CSC,actuall :-)

[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 2ee136dfe753e56dbf7dd3781432ad7a72fc769b..6a57c4a003f4e134be9a636e5de75987dbc6733c 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteTypes.ml
+++ b/helm/software/components/grafite_engine/grafiteTypes.ml
@@ -100,6 +100,48 @@ let get_estatus x =
   | CommandMode e -> e
 ;;
 
+let set_estatus e x =
+ { x with ng_status =
+   match x.ng_status with
+      ProofMode t ->
+       ProofMode
+        {t with NTacStatus.istatus =
+         {t.NTacStatus.istatus with NTacStatus.estatus = e}}
+    | CommandMode _ -> CommandMode e}
+;;
+
+let get_rstatus x = (get_estatus x).NEstatus.rstatus;;
+
+let get_hstatus x = (get_rstatus x).NRstatus.uhint_db;;
+
+let get_library_db x = (get_rstatus x).NRstatus.library_db;;
+
+let get_dump x = (get_rstatus x).NRstatus.dump;;
+
+let set_rstatus h x =
+ let estatus = get_estatus x in
+  set_estatus { estatus with NEstatus.rstatus = h } x
+;;
+
+let set_hstatus h x =
+ let rstatus = get_rstatus x in
+  set_rstatus { rstatus with NRstatus.uhint_db = h} x
+;;
+
+let set_library_db h x =
+ let rstatus = get_rstatus x in
+  set_rstatus { rstatus with NRstatus.library_db = h} x
+;;
+
+let set_dump h x =
+ let estatus = get_estatus x in
+  set_estatus
+  { estatus with NEstatus.rstatus =
+     { estatus.NEstatus.rstatus with
+        NRstatus.dump = h}}
+  x
+;;
+
 let get_current_proof status =
   match status.proof_status with
   | Incomplete_proof { proof = p } -> p