Just ignore anything in between [[ and ]] in the scanner, which is better that failing with a parse error. Fixes #1158 Fixes #2286