aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--toplevel/metasyntax.ml6
1 files changed, 5 insertions, 1 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index f9721e2d8..60d600ca1 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -306,6 +306,9 @@ let split_notation_string str =
let out_nt = function NonTerminal x -> x | _ -> assert false
+let msg_expected_form_of_recursive_notation =
+ "In the notation, the special symbol \"..\" must occur in\na configuration of the form \"x symbs .. symbs y\"."
+
let rec find_pattern nt xl = function
| Break n as x :: l, Break n' :: l' when Int.equal n n' ->
find_pattern nt (x::xl) (l,l')
@@ -318,13 +321,14 @@ let rec find_pattern nt xl = function
| _, Terminal s :: _ | Terminal s :: _, _ ->
error ("The token \""^s^"\" occurs on one side of \"..\" but not on the other side.")
| _, [] ->
- error ("The special symbol \"..\" must occur in a configuration of the form\n\"x symbs .. symbs y\".")
+ error msg_expected_form_of_recursive_notation
| ((SProdList _ | NonTerminal _) :: _), _ | _, (SProdList _ :: _) ->
anomaly "Only Terminal or Break expected on left, non-SProdList on right"
let rec interp_list_parser hd = function
| [] -> [], List.rev hd
| NonTerminal id :: tl when Id.equal id ldots_var ->
+ if List.is_empty hd then error msg_expected_form_of_recursive_notation;
let hd = List.rev hd in
let ((x,y,sl),tl') = find_pattern (List.hd hd) [] (List.tl hd,tl) in
let xyl,tl'' = interp_list_parser [] tl' in