--- a/src/Pure/General/symbol_pos.ML Wed Jan 20 00:06:48 2016 +0100
+++ b/src/Pure/General/symbol_pos.ML Wed Jan 20 14:32:56 2016 +0100
@@ -180,15 +180,15 @@
Scan.repeat1 (Scan.depend (fn (depth: int option) =>
(case depth of
SOME d =>
- $$ "\\<open>" >> pair (SOME (d + 1)) ||
+ $$ Symbol.open_ >> pair (SOME (d + 1)) ||
(if d > 0 then
- Scan.one (fn (s, _) => s <> "\\<close>" andalso Symbol.not_eof s) >> pair depth ||
- $$ "\\<close>" >> pair (if d = 1 then NONE else SOME (d - 1))
+ Scan.one (fn (s, _) => s <> Symbol.close andalso Symbol.not_eof s) >> pair depth ||
+ $$ Symbol.close >> pair (if d = 1 then NONE else SOME (d - 1))
else Scan.fail)
| NONE => Scan.fail)));
fun scan_cartouche err_prefix =
- Scan.ahead ($$ "\\<open>") |--
+ Scan.ahead ($$ Symbol.open_) |--
!!! (fn () => err_prefix ^ "unclosed text cartouche")
(Scan.provide is_none (SOME 0) scan_cartouche_depth);