diff options
| author | Pierre Roux | 2018-10-20 11:19:28 +0200 |
|---|---|---|
| committer | Pierre Roux | 2019-04-02 00:02:12 +0200 |
| commit | a95aacce6cc32726b494d4cc694da49eae86cf96 (patch) | |
| tree | 07caf6e22fd6ae991786cec51bf304ecd011bc02 /plugins/ssr | |
| parent | 1c8fd0f7134bcc295e31613c981ef4ef2c21af35 (diff) | |
Rename the INT token to NUMERAL
In anticipation of future uses of this token for non integer numerals.
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrparser.mlg | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 9931305832..457b333a16 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -224,20 +224,20 @@ let test_ssrslashnum b1 b2 strm = match Util.stream_nth 0 strm with | Tok.KEYWORD "/" -> (match Util.stream_nth 1 strm with - | Tok.INT _ when b1 -> + | Tok.NUMERAL _ when b1 -> (match Util.stream_nth 2 strm with | Tok.KEYWORD "=" | Tok.KEYWORD "/=" when not b2 -> () | Tok.KEYWORD "/" -> if not b2 then () else begin match Util.stream_nth 3 strm with - | Tok.INT _ -> () + | Tok.NUMERAL _ -> () | _ -> raise Stream.Failure end | _ -> raise Stream.Failure) | Tok.KEYWORD "/" when not b1 -> (match Util.stream_nth 2 strm with | Tok.KEYWORD "=" when not b2 -> () - | Tok.INT _ when b2 -> + | Tok.NUMERAL _ when b2 -> (match Util.stream_nth 3 strm with | Tok.KEYWORD "=" -> () | _ -> raise Stream.Failure) @@ -248,7 +248,7 @@ let test_ssrslashnum b1 b2 strm = | Tok.KEYWORD "//" when not b1 -> (match Util.stream_nth 1 strm with | Tok.KEYWORD "=" when not b2 -> () - | Tok.INT _ when b2 -> + | Tok.NUMERAL _ when b2 -> (match Util.stream_nth 2 strm with | Tok.KEYWORD "=" -> () | _ -> raise Stream.Failure) |