equal
deleted
inserted
replaced
186 fun check_level i = |
186 fun check_level i = |
187 if i > 0 then Scan.succeed () |
187 if i > 0 then Scan.succeed () |
188 else Scan.fail_with (K "Bad nesting of meta-comments"); |
188 else Scan.fail_with (K "Bad nesting of meta-comments"); |
189 |
189 |
190 val ignore = |
190 val ignore = |
191 Scan.depend (fn i => opt_newline |-- P.position (Scan.one T.is_begin_ignore) >> pair (i + 1)) || |
191 Scan.depend (fn i => P.position (Scan.one T.is_begin_ignore) >> pair (i + 1)) || |
192 Scan.depend (fn i => P.position (Scan.one T.is_end_ignore) --| check_level i >> pair (i - 1)); |
192 Scan.depend (fn i => P.position (Scan.one T.is_end_ignore) --| |
|
193 (opt_newline -- check_level i) >> pair (i - 1)); |
193 |
194 |
194 val ignore_cmd = Scan.state -- ignore |
195 val ignore_cmd = Scan.state -- ignore |
195 >> (fn (i, (x, pos)) => (false, (None, ((Latex.Basic x, ("", pos)), i)))); |
196 >> (fn (i, (x, pos)) => (false, (None, ((Latex.Basic x, ("", pos)), i)))); |
196 |
197 |
197 |
198 |