# HG changeset patch
# User oheimb
# Date 1039184190 -3600
# Node ID 452ff5d0b69d378c09039aa6c73397e2d9aae7c2
# Parent  ff140d072bc900ac8d41076ddf41f9bd0964243c
corrected swallowing of newlines after end-of-ignore

diff -r ff140d072bc9 -r 452ff5d0b69d src/Pure/Isar/isar_output.ML
--- a/src/Pure/Isar/isar_output.ML	Fri Dec 06 11:09:02 2002 +0100
+++ b/src/Pure/Isar/isar_output.ML	Fri Dec 06 15:16:30 2002 +0100
@@ -189,8 +189,7 @@
 
 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) --|
-    (opt_newline -- check_level i) >> pair (i - 1));
+  Scan.depend (fn i => P.position (Scan.one T.is_end_ignore) --| check_level i >> pair (i - 1));
 
 val ignore_cmd = Scan.state -- ignore
   >> (fn (i, (x, pos)) => (false, (None, ((Latex.Basic x, ("", pos)), i))));