diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-04-23 14:55:11 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-04-23 16:02:45 +0200 |
| commit | 16d301bab5b7dec53be4786b3b6815bca54ae539 (patch) | |
| tree | c595fc1fafd00a08cb91e53002610df867cf5eed /toplevel/mltop.ml | |
| parent | 915c8f15965fe8e7ee9d02a663fd890ef80539ad (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 'toplevel/mltop.ml')
| -rw-r--r-- | toplevel/mltop.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml index 0b6fc48c4..a7fb7a58f 100644 --- a/toplevel/mltop.ml +++ b/toplevel/mltop.ml @@ -164,7 +164,7 @@ let add_rec_ml_dir unix_path = let convert_string d = try Names.Id.of_string d with UserError _ -> - msg_warning (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)")); + msg_warning (str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)"); raise Exit let add_rec_path ~unix_path ~coq_root ~implicit = @@ -184,7 +184,7 @@ let add_rec_path ~unix_path ~coq_root ~implicit = let () = List.iter add dirs in Loadpath.add_load_path unix_path ~implicit coq_root else - msg_warning (str ("Cannot open " ^ unix_path)) + msg_warning (str "Cannot open " ++ str unix_path) (* convertit un nom quelconque en nom de fichier ou de module *) let mod_of_name name = @@ -321,13 +321,13 @@ let reset_loaded_modules () = loaded_modules := [] let if_verbose_load verb f name ?path fname = if not verb then f name ?path fname else - let info = "[Loading ML file "^fname^" ..." in + let info = str "[Loading ML file " ++ str fname ++ str " ..." in try let path = f name ?path fname in - msg_info (str (info^" done]")); + msg_info (info ++ str " done]"); path with reraise -> - msg_info (str (info^" failed]")); + msg_info (info ++ str " failed]"); raise reraise (** Load a module for the first time (i.e. dynlink it) @@ -340,7 +340,8 @@ let trigger_ml_object verb cache reinit ?path name = add_loaded_module name (known_module_path name); if cache then perform_cache_obj name end else if not has_dynlink then - error ("Dynamic link not supported (module "^name^")") + errorlabstrm "Mltop.trigger_ml_object" + (str "Dynamic link not supported (module " ++ str name ++ str ")") else begin let file = file_of_name (Option.default name path) in let path = |