aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/metasyntax.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 /toplevel/metasyntax.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 'toplevel/metasyntax.ml')
-rw-r--r--toplevel/metasyntax.ml25
1 files changed, 15 insertions, 10 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 639ec1e6e..f4fabc4d3 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -387,7 +387,8 @@ let rec find_pattern nt xl = function
| _, Break s :: _ | Break s :: _, _ ->
error ("A break occurs on one side of \"..\" but not on the other side.")
| _, Terminal s :: _ | Terminal s :: _, _ ->
- error ("The token \""^s^"\" occurs on one side of \"..\" but not on the other side.")
+ errorlabstrm "Metasyntax.find_pattern"
+ (str "The token \"" ++ str s ++ str "\" occurs on one side of \"..\" but not on the other side.")
| _, [] ->
error msg_expected_form_of_recursive_notation
| ((SProdList _ | NonTerminal _) :: _), _ | _, (SProdList _ :: _) ->
@@ -448,7 +449,8 @@ let rec get_notation_vars = function
let vars = get_notation_vars sl in
if Id.equal id ldots_var then vars else
if Id.List.mem id vars then
- error ("Variable "^Id.to_string id^" occurs more than once.")
+ errorlabstrm "Metasyntax.get_notation_vars"
+ (str "Variable " ++ pr_id id ++ str " occurs more than once.")
else
id::vars
| (Terminal _ | Break _) :: sl -> get_notation_vars sl
@@ -461,8 +463,8 @@ let analyze_notation_tokens l =
recvars, List.subtract Id.equal vars (List.map snd recvars), l
let error_not_same_scope x y =
- error ("Variables "^Id.to_string x^" and "^Id.to_string y^
- " must be in the same scope.")
+ errorlabstrm "Metasyntax.error_not_name_scope"
+ (str "Variables " ++ pr_id x ++ str " and " ++ pr_id y ++ str " must be in the same scope.")
(**********************************************************************)
(* Build pretty-printing rules *)
@@ -710,7 +712,7 @@ let is_not_small_constr = function
let rec define_keywords_aux = function
| GramConstrNonTerminal(e,Some _) as n1 :: GramConstrTerminal(IDENT k) :: l
when is_not_small_constr e ->
- Flags.if_verbose msg_info (strbrk ("Identifier '"^k^"' now a keyword"));
+ Flags.if_verbose msg_info (str "Identifier '" ++ str k ++ str "' now a keyword");
Lexer.add_keyword k;
n1 :: GramConstrTerminal(KEYWORD k) :: define_keywords_aux l
| n :: l -> n :: define_keywords_aux l
@@ -719,7 +721,7 @@ let rec define_keywords_aux = function
(* Ensure that IDENT articulation terminal symbols are keywords *)
let define_keywords = function
| GramConstrTerminal(IDENT k)::l ->
- Flags.if_verbose msg_info (strbrk ("Identifier '"^k^"' now a keyword"));
+ Flags.if_verbose msg_info (str "Identifier '" ++ str k ++ str "' now a keyword");
Lexer.add_keyword k;
GramConstrTerminal(KEYWORD k) :: define_keywords_aux l
| l -> define_keywords_aux l
@@ -804,7 +806,7 @@ let pr_level ntn (from,args) =
let error_incompatible_level ntn oldprec prec =
errorlabstrm ""
- (str ("Notation "^ntn^" is already defined") ++ spc() ++
+ (str "Notation " ++ str ntn ++ str " is already defined" ++ spc() ++
pr_level ntn oldprec ++
spc() ++ str "while it is now required to be" ++ spc() ++
pr_level ntn prec ++ str ".")
@@ -871,14 +873,16 @@ let interp_modifiers modl =
| SetEntryType (s,typ) :: l ->
let id = Id.of_string s in
if Id.List.mem_assoc id etyps then
- error (s^" is already assigned to an entry or constr level.");
+ errorlabstrm "Metasyntax.interp_modifiers"
+ (str s ++ str " is already assigned to an entry or constr level.");
interp assoc level ((id,typ)::etyps) format extra l
| SetItemLevel ([],n) :: l ->
interp assoc level etyps format extra l
| SetItemLevel (s::idl,n) :: l ->
let id = Id.of_string s in
if Id.List.mem_assoc id etyps then
- error (s^" is already assigned to an entry or constr level.");
+ errorlabstrm "Metasyntax.interp_modifiers"
+ (str s ++ str " is already assigned to an entry or constr level.");
let typ = ETConstr (n,()) in
interp assoc level ((id,typ)::etyps) format extra (SetItemLevel (idl,n)::l)
| SetLevel n :: l ->
@@ -905,7 +909,8 @@ let check_infix_modifiers modifiers =
let check_useless_entry_types recvars mainvars etyps =
let vars = let (l1,l2) = List.split recvars in l1@l2@mainvars in
match List.filter (fun (x,etyp) -> not (List.mem x vars)) etyps with
- | (x,_)::_ -> error (Id.to_string x ^ " is unbound in the notation.")
+ | (x,_)::_ -> errorlabstrm "Metasyntax.check_useless_entry_types"
+ (pr_id x ++ str " is unbound in the notation.")
| _ -> ()
let no_syntax_modifiers = function