src/Pure/General/symbol_pos.ML
changeset 58854 b979c781c2db
parent 58850 1bb0ad7827b4
child 58864 505a8150368a
     1.1 --- a/src/Pure/General/symbol_pos.ML	Fri Oct 31 21:48:40 2014 +0100
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Fri Oct 31 22:02:49 2014 +0100
     1.3 @@ -111,7 +111,7 @@
     1.4  fun scan_str q err_prefix =
     1.5    $$$ "\\" |-- !!! (fn () => err_prefix ^ "bad escape character in string")
     1.6      ($$$ q || $$$ "\\" || char_code) ||
     1.7 -  Scan.one (fn (s, _) => s <> q andalso s <> "\\" andalso Symbol.is_regular s) >> single;
     1.8 +  Scan.one (fn (s, _) => s <> q andalso s <> "\\" andalso Symbol.not_eof s) >> single;
     1.9  
    1.10  fun scan_strs q err_prefix =
    1.11    Scan.ahead ($$ q) |--
    1.12 @@ -164,7 +164,7 @@
    1.13    Scan.repeat1 (Scan.depend (fn (d: int) =>
    1.14      $$ "\\<open>" >> pair (d + 1) ||
    1.15        (if d > 0 then
    1.16 -        Scan.one (fn (s, _) => s <> "\\<close>" andalso Symbol.is_regular s) >> pair d ||
    1.17 +        Scan.one (fn (s, _) => s <> "\\<close>" andalso Symbol.not_eof s) >> pair d ||
    1.18          $$ "\\<close>" >> pair (d - 1)
    1.19        else Scan.fail)));
    1.20  
    1.21 @@ -198,7 +198,7 @@
    1.22    Scan.depend (fn (d: int) => $$$ "(" @@@ $$$ "*" >> pair (d + 1)) ||
    1.23    Scan.depend (fn 0 => Scan.fail | d => $$$ "*" @@@ $$$ ")" >> pair (d - 1)) ||
    1.24    Scan.lift ($$$ "*" --| Scan.ahead (~$$$ ")")) ||
    1.25 -  Scan.lift (Scan.one (fn (s, _) => s <> "*" andalso Symbol.is_regular s)) >> single;
    1.26 +  Scan.lift (Scan.one (fn (s, _) => s <> "*" andalso Symbol.not_eof s)) >> single;
    1.27  
    1.28  val scan_cmts = Scan.pass 0 (Scan.repeat scan_cmt >> flat);
    1.29