]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/grafite_engine/grafiteEngine.ml
Bug fixed: singleton application.
[helm.git] / helm / software / components / grafite_engine / grafiteEngine.ml
index 3a108acccc5c079ee7e2426edf0d3490f60628c1..f1aea02da0a71efd0bece6fa26c0df667a5cc685 100644 (file)
@@ -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")