# HG changeset patch # User oheimb # Date 1042029284 -3600 # Node ID a918c547cd4dd01c8ca3570238b217b561d8c058 # Parent 77a1e723151d32f0ab08bbe0677a9a6717e86f66 corrected swallowing of newlines after end-of-ignore: rollback diff -r 77a1e723151d -r a918c547cd4d src/Pure/Isar/isar_output.ML --- a/src/Pure/Isar/isar_output.ML Tue Jan 07 18:08:17 2003 +0100 +++ b/src/Pure/Isar/isar_output.ML Wed Jan 08 13:34:44 2003 +0100 @@ -188,8 +188,8 @@ else Scan.fail_with (K "Bad nesting of meta-comments"); val ignore = - Scan.depend (fn i => P.position (Scan.one T.is_begin_ignore) >> pair (i + 1)) || - Scan.depend (fn i => P.position (Scan.one T.is_end_ignore) --| + Scan.depend (fn i => opt_newline |-- P.position (Scan.one T.is_begin_ignore) >> pair (i + 1)) || + Scan.depend (fn i => P.position (Scan.one T.is_end_ignore) --| (opt_newline -- check_level i) >> pair (i - 1)); val ignore_cmd = Scan.state -- ignore