aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/libobject.ml
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-04-23 14:55:11 +0200
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-04-23 16:02:45 +0200
commit16d301bab5b7dec53be4786b3b6815bca54ae539 (patch)
treec595fc1fafd00a08cb91e53002610df867cf5eed /library/libobject.ml
parent915c8f15965fe8e7ee9d02a663fd890ef80539ad (diff)
Remove almost all the uses of string concatenation when building error messages.
Since error messages are ultimately passed to Format, which has its own buffers for concatenating strings, using concatenation for preparing error messages just doubles the workload and increases memory pressure.
Diffstat (limited to 'library/libobject.ml')
-rw-r--r--library/libobject.ml5
1 files changed, 2 insertions, 3 deletions
diff --git a/library/libobject.ml b/library/libobject.ml
index 5f2a2127d..74930d76e 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)}