From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 8 May 2009 16:47:23 +0000 (+0000)
Subject: 1) better implementation of NObj that now calls recursively NQed
X-Git-Tag: make_still_working~4007
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ef9c7ecffee95d77cd10fa2d37bd2b26b94b9eb9;p=helm.git

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 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