undo/serialization for universes implemented

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

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index b6a8786f22e2dc933ac1bdf2756cb286238ccf38..5d1ea50962f211c333732ebc1fafb1622194b640 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -475,7 +475,10 @@ let basic_eval_unification_hint (t,n) status =
 ;;
 
 let inject_unification_hint =
- let basic_eval_unification_hint (t,n) ~refresh_uri_in_term =
+ let basic_eval_unification_hint (t,n) 
+   ~refresh_uri_in_universe 
+   ~refresh_uri_in_term
+ =
   let t = refresh_uri_in_term t in basic_eval_unification_hint (t,n)
  in
   NRstatus.Serializer.register "unification_hints" basic_eval_unification_hint
@@ -488,6 +491,29 @@ let eval_unification_hint status t n =
  let t = NCicUntrusted.apply_subst subst [] t in
  let status = basic_eval_unification_hint (t,n) status in
  let dump = inject_unification_hint (t,n)::status#dump in
+ let status = status#set_dump dump in
+  status,`New []
+;;
+
+let basic_eval_add_constraint (s,u1,u2) status =
+ NCicLibrary.add_constraint status s u1 u2
+;;
+
+let inject_constraint =
+ let basic_eval_add_constraint (s,u1,u2) 
+       ~refresh_uri_in_universe 
+       ~refresh_uri_in_term
+ =
+  let u1 = refresh_uri_in_universe u1 in 
+  let u2 = refresh_uri_in_universe u2 in 
+  basic_eval_add_constraint (s,u1,u2)
+ in
+  NRstatus.Serializer.register "constraints" basic_eval_add_constraint
+;;
+
+let eval_add_constraint status s u1 u2 = 
+ let status = basic_eval_add_constraint (s,u1,u2) status in
+ let dump = inject_constraint (s,u1,u2)::status#dump in
  let status = status#set_dump dump in
   status,`Old []
 ;;
@@ -727,8 +753,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
            eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
         | _ -> status,`New [])
   | GrafiteAst.NUnivConstraint (loc,strict,u1,u2) ->
-      NCicEnvironment.add_constraint strict [false,u1] [false,u2];
-      status, `New [u1;u2]
+      eval_add_constraint status strict [false,u1] [false,u2]
 ;;
 
 let rec eval_command = {ec_go = fun ~disambiguate_command opts status