equal
deleted
inserted
replaced
353 |
353 |
354 val ignore = |
354 val ignore = |
355 Scan.depend (fn d => opt_newline |-- Scan.one Token.is_begin_ignore |
355 Scan.depend (fn d => opt_newline |-- Scan.one Token.is_begin_ignore |
356 >> pair (d + 1)) || |
356 >> pair (d + 1)) || |
357 Scan.depend (fn d => Scan.one Token.is_end_ignore --| |
357 Scan.depend (fn d => Scan.one Token.is_end_ignore --| |
358 (if d = 0 then Scan.fail_with (K "Bad nesting of meta-comments") else opt_newline) |
358 (if d = 0 then Scan.fail_with (K (fn () => "Bad nesting of meta-comments")) else opt_newline) |
359 >> pair (d - 1)); |
359 >> pair (d - 1)); |
360 |
360 |
361 val tag = (improper -- Parse.$$$ "%" -- improper) |-- Parse.!!! (Parse.tag_name --| blank_end); |
361 val tag = (improper -- Parse.$$$ "%" -- improper) |-- Parse.!!! (Parse.tag_name --| blank_end); |
362 |
362 |
363 val locale = |
363 val locale = |