1.1 --- a/src/Pure/Isar/outer_syntax.ML	Thu Oct 21 18:44:05 1999 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Thu Oct 21 18:44:34 1999 +0200
     1.3 @@ -339,16 +339,23 @@
     1.4  
     1.5  local
     1.6  
     1.7 +val indent_prop = Scan.one T.is_indent -- Scan.one T.is_proper;
     1.8 +val improp = Scan.unless indent_prop (Scan.one (not o T.is_proper));
     1.9 +val improper_keep_indent = Scan.repeat improp;
    1.10 +
    1.11  val improper = Scan.any (not o T.is_proper);
    1.12 +
    1.13 +val improper_end =
    1.14 +  (improper -- semicolon) |-- improper_keep_indent ||
    1.15 +  improper_keep_indent;
    1.16 +
    1.17  val markup = Scan.one (T.is_kind T.Command andf is_markup o T.val_of) >> T.val_of;
    1.18  val verbatim = Scan.one (T.is_kind T.Command andf is_verbatim o T.val_of);
    1.19  
    1.20  val present_token =
    1.21 -  improper |-- markup -- (improper |-- P.text --| (improper -- Scan.option semicolon -- improper))
    1.22 -    >> Present.markup_token ||
    1.23 +  improper |-- markup -- (improper |-- P.text --| improper_end) >> Present.markup_token ||
    1.24    (P.$$$ "--" >> K "cmt") -- (improper |-- P.text) >> Present.markup_token ||
    1.25 -  (improper -- verbatim -- improper) |-- P.text --| (improper -- Scan.option semicolon -- improper)
    1.26 -    >> Present.verbatim_token ||
    1.27 +  (improper -- verbatim -- improper) |-- P.text --| improper_end >> Present.verbatim_token ||
    1.28    Scan.one T.not_eof >> Present.basic_token;
    1.29  
    1.30  in