1) better implementation of NObj that now calls recursively NQed

   to avoid code duplication
2) NQed now calls the kernel to check the object, since add_obj is too
   low level for that (this makes a huge difference with the previous
   architecture, but will probably break when dealing with undo)

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 4ab7412d832c60f4e0c0c0aab339e5ef9f2a652e..b1cedb077bec99b5132da5d5f87cab8db0cacea6 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -761,6 +761,7 @@ prerr_endline "CSC: here we should fix the height!!!";
                uri,height,[],[],
                 NCicUntrusted.map_obj_kind (NCicUntrusted.apply_subst subst) obj
               in
+               NCicTypeChecker.typecheck_obj obj;
                NCicLibrary.add_obj uri obj;
                {status with 
                  GrafiteTypes.ng_status = 
@@ -780,26 +781,20 @@ prerr_endline "CSC: here we should fix the height!!!";
       GrafiteDisambiguate.disambiguate_nobj lexicon_status
        ~baseuri:(GrafiteTypes.get_baseuri status) (text,prefix_len,obj) in
      let uri,height,nmenv,nsubst,nobj = obj in
+     let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
+     let status =
+      { status with
+         GrafiteTypes.ng_status = 
+          GrafiteTypes.ProofMode
+           { NTacStatus.gstatus = ninitial_stack; 
+             istatus = { NTacStatus.pstatus = obj; lstatus = lexicon_status}}
+           }
+     in
      (match nmenv with
-        [] ->
-          (* CSC: cut&paste code from NQed *)
-          let obj =
-prerr_endline "CSC: here we should fix the height!!!";
-           uri,height,[],[],
-            NCicUntrusted.map_obj_kind (NCicUntrusted.apply_subst nsubst) nobj
-          in
-           NCicLibrary.add_obj uri obj;
-           {status with 
-             GrafiteTypes.ng_status=GrafiteTypes.CommandMode lexicon_status },
-           `New [uri]
-      | _ ->
-        let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
-        { status with
-           GrafiteTypes.ng_status = 
-            GrafiteTypes.ProofMode
-             { NTacStatus.gstatus = ninitial_stack; 
-               istatus = { NTacStatus.pstatus = obj; lstatus = lexicon_status}}
-             },`New [])
+         [] ->
+          eval_command.ec_go ~disambiguate_command opts status
+           ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
+       | _ -> status,`New [])
   | GrafiteAst.Obj (loc,obj) ->
      let ext,name =
       match obj with