From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 17 Jul 2009 19:51:37 +0000 (+0000)
Subject: 1) the user is notified when a new object is defined
X-Git-Tag: make_still_working~3661
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0c8e6ee3543b6554b3f3f4ead631264e0169be7b;p=helm.git

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 b5f503497..3976978f7 100644
--- 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 ->