- //public Element _tilde__slash__tilde_(final Element r) { return Repeat.maximal(r); }
- public Object _plus__slash_(final Element r, Object s) {
- if (s instanceof String) s = CharToken.string((String)s);
- return new Rep(r, (Element)s, false, false);
- }
- public Object _star__slash_(final Element r, Object s) {
- if (s instanceof String) s = CharToken.string((String)s);
- return new Rep(r, (Element)s, false, true);
- }
- //public Element _star__slash_(final Element r, Element s) { return Repeat.many0(r, s); }
+ public Object _plus__slash_(final Element r, Object s) { return new Rep(r, (Element)s, false, false); }
+ public Object _star__slash_(final Element r, Object s) { return new Rep(r, (Element)s, false, true); }