FIX OF THE PREVIOUS EXPERIMENTAL COMMIT:

[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 6a57c4a003f4e134be9a636e5de75987dbc6733c..0b9a4a7da8e161f75aa0d3ece109c6548f248fc7 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteTypes.ml
+++ b/helm/software/components/grafite_engine/grafiteTypes.ml
@@ -78,22 +78,6 @@ let set_lexicon new_lexicon_status new_grafite_status =
                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
@@ -110,19 +94,32 @@ let set_estatus e x =
     | CommandMode _ -> CommandMode e}
 ;;
 
-let get_rstatus x = (get_estatus x).NEstatus.rstatus;;
+let get_dstatus x = (get_estatus x).NEstatus.rstatus;;
+
+let get_rstatus x = (get_dstatus x).NRstatus.refiner_status;;
 
 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 get_dump x = (get_dstatus x).NRstatus.dump;;
 
-let set_rstatus h x =
+let set_dstatus h x =
  let estatus = get_estatus x in
   set_estatus { estatus with NEstatus.rstatus = h } x
 ;;
 
+let set_rstatus h x =
+ let dstatus = get_dstatus x in
+  set_dstatus { dstatus with NRstatus.refiner_status = h } x
+;;
+
+let set_coercions db x = 
+ let rstatus = get_rstatus x in
+  set_rstatus { rstatus with NRstatus.coerc_db = db } x
+;;
+
+
 let set_hstatus h x =
  let rstatus = get_rstatus x in
   set_rstatus { rstatus with NRstatus.uhint_db = h} x
@@ -275,8 +272,4 @@ 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 
-;;
-
+let get_coercions x = (get_rstatus x).NRstatus.coerc_db;;