1.1 --- a/src/Pure/Isar/antiquote.ML	Mon Jan 28 22:27:21 2008 +0100
     1.2 +++ b/src/Pure/Isar/antiquote.ML	Mon Jan 28 22:27:23 2008 +0100
     1.3 @@ -34,9 +34,8 @@
     1.4  local
     1.5  
     1.6  val scan_txt =
     1.7 -  T.scan_blank ||
     1.8 -  T.keep_line ($$ "@" --| Scan.ahead (~$$ "{")) ||
     1.9 -  T.keep_line (Scan.one (fn s => s <> "@" andalso Symbol.is_regular s));
    1.10 +  T.count ($$ "@" --| Scan.ahead (~$$ "{")) ||
    1.11 +  T.count (Scan.one (fn s => s <> "@" andalso Symbol.is_regular s));
    1.12  
    1.13  fun escape "\\" = "\\\\"
    1.14    | escape "\"" = "\\\""
    1.15 @@ -45,14 +44,13 @@
    1.16  val quote_escape = Library.quote o implode o map escape o Symbol.explode;
    1.17  
    1.18  val scan_ant =
    1.19 -  T.scan_blank ||
    1.20    T.scan_string >> quote_escape ||
    1.21 -  T.keep_line (Scan.one (fn s => s <> "}" andalso Symbol.is_regular s));
    1.22 +  T.count (Scan.one (fn s => s <> "}" andalso Symbol.is_regular s));
    1.23  
    1.24  val scan_antiq =
    1.25 -  T.keep_line ($$ "@" -- $$ "{") |--
    1.26 +  T.count ($$ "@") |-- T.count ($$ "{") |--
    1.27      T.!!! "missing closing brace of antiquotation"
    1.28 -      (Scan.repeat scan_ant >> implode) --| T.keep_line ($$ "}");
    1.29 +      (Scan.repeat scan_ant >> implode) --| T.count ($$ "}");
    1.30  
    1.31  in
    1.32