scan only one line, for more detailed positions;
authorwenzelm
Tue Dec 12 18:53:40 2017 +0100 (17 months ago)
changeset 671934ade0d387429
parent 67192 26f548370e8d
child 67194 1c0a6a957114
scan only one line, for more detailed positions;
src/Pure/General/antiquote.ML
     1.1 --- a/src/Pure/General/antiquote.ML	Tue Dec 12 17:53:59 2017 +0100
     1.2 +++ b/src/Pure/General/antiquote.ML	Tue Dec 12 18:53:40 2017 +0100
     1.3 @@ -76,11 +76,15 @@
     1.4  
     1.5  val err_prefix = "Antiquotation lexical error: ";
     1.6  
     1.7 +val scan_nl = Scan.one (fn (s, _) => s = "\n") >> single;
     1.8 +
     1.9  val scan_txt =
    1.10 +  scan_nl ||
    1.11    Scan.repeats1
    1.12     (Scan.many1 (fn (s, _) =>
    1.13 -      not (Symbol.is_control s) andalso s <> Symbol.open_ andalso s <> "@" andalso Symbol.not_eof s) ||
    1.14 -    $$$ "@" --| Scan.ahead (~$$ "{"));
    1.15 +      not (Symbol.is_control s) andalso s <> Symbol.open_ andalso s <> "@" andalso
    1.16 +        s <> "\n" andalso Symbol.not_eof s) ||
    1.17 +    $$$ "@" --| Scan.ahead (~$$ "{")) @@@ Scan.optional scan_nl [];
    1.18  
    1.19  val scan_antiq_body =
    1.20    Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 ||