src/Pure/General/symbol_pos.ML
changeset 62210 e068ea693678
parent 61707 d5ddd022a451
child 62239 6ee95b93fbed
     1.1 --- a/src/Pure/General/symbol_pos.ML	Wed Jan 20 00:06:48 2016 +0100
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Wed Jan 20 14:32:56 2016 +0100
     1.3 @@ -180,15 +180,15 @@
     1.4    Scan.repeat1 (Scan.depend (fn (depth: int option) =>
     1.5      (case depth of
     1.6        SOME d =>
     1.7 -        $$ "\\<open>" >> pair (SOME (d + 1)) ||
     1.8 +        $$ Symbol.open_ >> pair (SOME (d + 1)) ||
     1.9            (if d > 0 then
    1.10 -            Scan.one (fn (s, _) => s <> "\\<close>" andalso Symbol.not_eof s) >> pair depth ||
    1.11 -            $$ "\\<close>" >> pair (if d = 1 then NONE else SOME (d - 1))
    1.12 +            Scan.one (fn (s, _) => s <> Symbol.close andalso Symbol.not_eof s) >> pair depth ||
    1.13 +            $$ Symbol.close >> pair (if d = 1 then NONE else SOME (d - 1))
    1.14            else Scan.fail)
    1.15      | NONE => Scan.fail)));
    1.16  
    1.17  fun scan_cartouche err_prefix =
    1.18 -  Scan.ahead ($$ "\\<open>") |--
    1.19 +  Scan.ahead ($$ Symbol.open_) |--
    1.20      !!! (fn () => err_prefix ^ "unclosed text cartouche")
    1.21        (Scan.provide is_none (SOME 0) scan_cartouche_depth);
    1.22