# HG changeset patch
# User wenzelm
# Date 1453296776 -3600
# Node ID e068ea69367813d1981c3efb09c459857bdba59f
# Parent  aed720a91f2f4adbcd123f6161da40bd59d0c53c
tuned signature (according to Scala version);

diff -r aed720a91f2f -r e068ea693678 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Wed Jan 20 00:06:48 2016 +0100
+++ b/src/Pure/General/pretty.ML	Wed Jan 20 14:32:56 2016 +0100
@@ -167,7 +167,7 @@
 val para = paragraph o text;
 
 fun quote prt = blk (1, [str "\"", prt, str "\""]);
-fun cartouche prt = blk (1, [str "\\<open>", prt, str "\\<close>"]);
+fun cartouche prt = blk (1, [str Symbol.open_, prt, str Symbol.close]);
 
 fun separate sep prts =
   flat (Library.separate [str sep, brk 1] (map single prts));
diff -r aed720a91f2f -r e068ea693678 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Wed Jan 20 00:06:48 2016 +0100
+++ b/src/Pure/General/symbol.ML	Wed Jan 20 14:32:56 2016 +0100
@@ -10,6 +10,8 @@
   val spaces: int -> string
   val STX: symbol
   val DEL: symbol
+  val open_: symbol
+  val close: symbol
   val space: symbol
   val comment: symbol
   val is_char: symbol -> bool
@@ -93,6 +95,9 @@
 val STX = chr 2;
 val DEL = chr 127;
 
+val open_ = "\\<open>";
+val close = "\\<close>";
+
 val space = chr 32;
 
 local
@@ -115,7 +120,7 @@
   String.isPrefix "\\<" s andalso String.isSuffix ">" s andalso not (String.isPrefix "\\<^" s);
 
 fun is_symbolic s =
-  s <> "\\<open>" andalso s <> "\\<close>" andalso raw_symbolic s;
+  s <> open_ andalso s <> close andalso raw_symbolic s;
 
 val is_symbolic_char = member (op =) (raw_explode "!#$%&*+-/<=>?@^_|~");
 
diff -r aed720a91f2f -r e068ea693678 src/Pure/General/symbol_pos.ML
--- 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);