From ef9c7ecffee95d77cd10fa2d37bd2b26b94b9eb9 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 8 May 2009 16:47:23 +0000
Subject: [PATCH] 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)

---
 .../grafite_engine/grafiteEngine.ml           | 33 ++++++++-----------
 1 file changed, 14 insertions(+), 19 deletions(-)

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 4ab7412d8..b1cedb077 100644
--- 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
-- 
2.39.2