()
| 9759 | } |
| 9760 | |
| 9761 | function patch() { |
| 9762 | if (typeof extra.tokens !== 'undefined') { |
| 9763 | extra.advance = advance; |
| 9764 | extra.scanRegExp = scanRegExp; |
| 9765 | |
| 9766 | advance = collectToken; |
| 9767 | scanRegExp = collectRegex; |
| 9768 | } |
| 9769 | } |
| 9770 | |
| 9771 | function unpatch() { |
| 9772 | if (typeof extra.scanRegExp === 'function') { |