# HG changeset patch
# User wenzelm
# Date 940524274 -7200
# Node ID cc6177e1efca472ee1a02b73c439fd73fa8d3296
# Parent  10fd5d922c972221ea60c58b65e20e4fec72c22e
markup: keep indentation;

diff -r 10fd5d922c97 -r cc6177e1efca src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Thu Oct 21 18:44:05 1999 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Thu Oct 21 18:44:34 1999 +0200
@@ -339,16 +339,23 @@
 
 local
 
+val indent_prop = Scan.one T.is_indent -- Scan.one T.is_proper;
+val improp = Scan.unless indent_prop (Scan.one (not o T.is_proper));
+val improper_keep_indent = Scan.repeat improp;
+
 val improper = Scan.any (not o T.is_proper);
+
+val improper_end =
+  (improper -- semicolon) |-- improper_keep_indent ||
+  improper_keep_indent;
+
 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);
 
 val present_token =
-  improper |-- markup -- (improper |-- P.text --| (improper -- Scan.option semicolon -- improper))
-    >> Present.markup_token ||
+  improper |-- markup -- (improper |-- P.text --| improper_end) >> Present.markup_token ||
   (P.$$$ "--" >> K "cmt") -- (improper |-- P.text) >> Present.markup_token ||
-  (improper -- verbatim -- improper) |-- P.text --| (improper -- Scan.option semicolon -- improper)
-    >> Present.verbatim_token ||
+  (improper -- verbatim -- improper) |-- P.text --| improper_end >> Present.verbatim_token ||
   Scan.one T.not_eof >> Present.basic_token;
 
 in