diff options
Diffstat (limited to 'library/libobject.ml')
| -rw-r--r-- | library/libobject.ml | 16 |
1 files changed, 12 insertions, 4 deletions
diff --git a/library/libobject.ml b/library/libobject.ml index 5f2a2127..85c830ea 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -7,6 +7,7 @@ (************************************************************************) open Libnames +open Pp (* The relax flag is used to make it possible to load files while ignoring failures to incorporate some objects. This can be useful when one @@ -33,15 +34,13 @@ type 'a object_declaration = { discharge_function : object_name * 'a -> 'a option; rebuild_function : 'a -> 'a } -let yell s = Errors.anomaly (Pp.str s) - let default_object s = { object_name = s; cache_function = (fun _ -> ()); load_function = (fun _ _ -> ()); open_function = (fun _ _ -> ()); subst_function = (fun _ -> - yell ("The object "^s^" does not know how to substitute!")); + Errors.anomaly (str "The object " ++ str s ++ str " does not know how to substitute!")); classify_function = (fun obj -> Keep obj); discharge_function = (fun _ -> None); rebuild_function = (fun x -> x)} @@ -102,7 +101,16 @@ let declare_object_full odecl = dyn_rebuild_function = rebuild }; (infun,outfun) -let declare_object odecl = fst (declare_object_full odecl) +(* The "try .. with .. " allows for correct printing when calling + declare_object a loading time. +*) + +let declare_object odecl = + try fst (declare_object_full odecl) + with e -> Errors.fatal_error (Errors.print e) (Errors.is_anomaly e) +let declare_object_full odecl = + try declare_object_full odecl + with e -> Errors.fatal_error (Errors.print e) (Errors.is_anomaly e) let missing_tab = (Hashtbl.create 17 : (string, unit) Hashtbl.t) |