1.1 --- a/src/Pure/Isar/outer_syntax.ML	Sat Apr 01 20:12:52 2000 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Sat Apr 01 20:13:33 2000 +0200
     1.3 @@ -359,9 +359,11 @@
     1.4    Scan.depend (fn 0 => Scan.fail | d => Scan.one T.is_end_ignore >> pair (d - 1)) ||
     1.5    Scan.lift (Scan.one (OuterLex.not_eof andf (not o OuterLex.is_end_ignore)));
     1.6  
     1.7 +val opt_newline = Scan.option (Scan.one T.is_newline);
     1.8 +
     1.9  val ignore_stuff =
    1.10 -  Scan.one T.is_begin_ignore |--
    1.11 -    P.!!!! (Scan.pass 0 (Scan.repeat ignore) -- Scan.one T.is_end_ignore);
    1.12 +  opt_newline -- Scan.one T.is_begin_ignore --
    1.13 +    P.!!!! (Scan.pass 0 (Scan.repeat ignore) -- Scan.one T.is_end_ignore -- opt_newline);
    1.14  
    1.15  val markup = Scan.one (T.is_kind T.Command andf is_markup o T.val_of) >> T.val_of;
    1.16  val verbatim = Scan.one (T.is_kind T.Command andf is_verbatim o T.val_of);