diff options
Diffstat (limited to 'toplevel/metasyntax.ml')
| -rw-r--r-- | toplevel/metasyntax.ml | 6 |
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 |