X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=f1aea02da0a71efd0bece6fa26c0df667a5cc685;hb=65792c85896dab2d3c69e7eafd8ff5c628260773;hp=3a108acccc5c079ee7e2426edf0d3490f60628c1;hpb=948bb5d710c5d7f3185b6fef76c8e71f247cc664;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 3a108accc..f1aea02da 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -957,7 +957,9 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
         let obj = uri,height,[],[],obj_kind in
          let status = NCicLibrary.add_obj status obj in
        prerr_endline (NCicPp.ppobj obj);
-         let objs = NCicElim.mk_elims obj in
+         let boxml = NCicElim.mk_elims obj in
+(*
+         let objs = [] in
          let timestamp,uris_rev =
            List.fold_left
             (fun (status,uris_rev) (uri,_,_,_,_) as obj ->
@@ -965,7 +967,19 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
                status,uri::uris_rev
             ) (status,[]) objs in
          let uris = uri::List.rev uris_rev in
-          status#set_ng_mode `CommandMode,`New uris
+*)
+         let status = status#set_ng_mode `CommandMode in
+let status = LexiconSync.add_aliases_for_objs status (`New [uri]) in
+         List.fold_left
+          (fun (status,uris) boxml ->
+            let status,nuris =
+             eval_ncommand opts status
+              ("",0,GrafiteAst.NObj (HExtlib.dummy_floc,boxml))
+            in
+             match uris,nuris with
+                `New uris, `New nuris -> status,`New (nuris@uris)
+              | _ -> assert false
+          ) (status,`New [] (* uris *)) boxml
   | GrafiteAst.NCopy (log,tgt,src_uri, map) ->
      if status#ng_mode <> `CommandMode then
       raise (GrafiteTypes.Command_error "Not in command mode")