# HG changeset patch
# User oheimb
# Date 1041959297 -3600
# Node ID 77a1e723151d32f0ab08bbe0677a9a6717e86f66
# Parent  58dc4ab362d0b9eed3b46d39006497e08b08876d
corrected swallowing of newlines after end-of-ignore (improved)

diff -r 58dc4ab362d0 -r 77a1e723151d src/Pure/Isar/isar_output.ML
--- a/src/Pure/Isar/isar_output.ML	Tue Jan 07 14:32:04 2003 +0100
+++ b/src/Pure/Isar/isar_output.ML	Tue Jan 07 18:08:17 2003 +0100
@@ -188,8 +188,9 @@
   else Scan.fail_with (K "Bad nesting of meta-comments");
 
 val 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) --| check_level i >> pair (i - 1));
+  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) --| 
+    (opt_newline -- check_level i) >> pair (i - 1));
 
 val ignore_cmd = Scan.state -- ignore
   >> (fn (i, (x, pos)) => (false, (None, ((Latex.Basic x, ("", pos)), i))));