1) the user is notified when a new object is defined

2) (very ugly) "detection" of elimination principles that cannot be defined

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index b5f503497590bca86fd161922f417d9d9d586c3c..3976978f71e5833b932c15090602b47152a2fff8 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -964,6 +964,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
         let obj = uri,height,[],[],obj_kind in
         let old_status = status in
         let status = NCicLibrary.add_obj status obj in
+        HLog.message ("New object: " ^ NUri.string_of_uri uri);
          (try
        (*prerr_endline (NCicPp.ppobj obj);*)
            let boxml = NCicElim.mk_elims obj in
@@ -981,13 +982,19 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
            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
+              try
+               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
+              with
+               NCicTypeChecker.TypeCheckerFailure msg
+                when Lazy.force msg =
+                "Sort elimination not allowed" ->
+                 status,uris
             ) (status,`New [] (* uris *)) boxml
           with
            exn ->