# HG changeset patch
# User wenzelm
# Date 954612813 -7200
# Node ID 39a695b0b1d7e3e49d3cf6b0d599fd1164b187aa
# Parent  f095f3b8181a60c055e2bd5c10d7851555b9c39f
presentation ignore stuff: swallow newline;

diff -r f095f3b8181a -r 39a695b0b1d7 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Sat Apr 01 20:12:52 2000 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Sat Apr 01 20:13:33 2000 +0200
@@ -359,9 +359,11 @@
   Scan.depend (fn 0 => Scan.fail | d => Scan.one T.is_end_ignore >> pair (d - 1)) ||
   Scan.lift (Scan.one (OuterLex.not_eof andf (not o OuterLex.is_end_ignore)));
 
+val opt_newline = Scan.option (Scan.one T.is_newline);
+
 val ignore_stuff =
-  Scan.one T.is_begin_ignore |--
-    P.!!!! (Scan.pass 0 (Scan.repeat ignore) -- Scan.one T.is_end_ignore);
+  opt_newline -- Scan.one T.is_begin_ignore --
+    P.!!!! (Scan.pass 0 (Scan.repeat ignore) -- Scan.one T.is_end_ignore -- opt_newline);
 
 val markup = Scan.one (T.is_kind T.Command andf is_markup o T.val_of) >> T.val_of;
 val verbatim = Scan.one (T.is_kind T.Command andf is_verbatim o T.val_of);