tuned signature (according to Scala version);
authorwenzelm
Wed Jan 20 14:32:56 2016 +0100 (2016-01-20)
changeset 62210e068ea693678
parent 62206 aed720a91f2f
child 62211 cc1557643ab1
tuned signature (according to Scala version);
src/Pure/General/pretty.ML
src/Pure/General/symbol.ML
src/Pure/General/symbol_pos.ML
     1.1 --- a/src/Pure/General/pretty.ML	Wed Jan 20 00:06:48 2016 +0100
     1.2 +++ b/src/Pure/General/pretty.ML	Wed Jan 20 14:32:56 2016 +0100
     1.3 @@ -167,7 +167,7 @@
     1.4  val para = paragraph o text;
     1.5  
     1.6  fun quote prt = blk (1, [str "\"", prt, str "\""]);
     1.7 -fun cartouche prt = blk (1, [str "\\<open>", prt, str "\\<close>"]);
     1.8 +fun cartouche prt = blk (1, [str Symbol.open_, prt, str Symbol.close]);
     1.9  
    1.10  fun separate sep prts =
    1.11    flat (Library.separate [str sep, brk 1] (map single prts));
     2.1 --- a/src/Pure/General/symbol.ML	Wed Jan 20 00:06:48 2016 +0100
     2.2 +++ b/src/Pure/General/symbol.ML	Wed Jan 20 14:32:56 2016 +0100
     2.3 @@ -10,6 +10,8 @@
     2.4    val spaces: int -> string
     2.5    val STX: symbol
     2.6    val DEL: symbol
     2.7 +  val open_: symbol
     2.8 +  val close: symbol
     2.9    val space: symbol
    2.10    val comment: symbol
    2.11    val is_char: symbol -> bool
    2.12 @@ -93,6 +95,9 @@
    2.13  val STX = chr 2;
    2.14  val DEL = chr 127;
    2.15  
    2.16 +val open_ = "\\<open>";
    2.17 +val close = "\\<close>";
    2.18 +
    2.19  val space = chr 32;
    2.20  
    2.21  local
    2.22 @@ -115,7 +120,7 @@
    2.23    String.isPrefix "\\<" s andalso String.isSuffix ">" s andalso not (String.isPrefix "\\<^" s);
    2.24  
    2.25  fun is_symbolic s =
    2.26 -  s <> "\\<open>" andalso s <> "\\<close>" andalso raw_symbolic s;
    2.27 +  s <> open_ andalso s <> close andalso raw_symbolic s;
    2.28  
    2.29  val is_symbolic_char = member (op =) (raw_explode "!#$%&*+-/<=>?@^_|~");
    2.30  
     3.1 --- a/src/Pure/General/symbol_pos.ML	Wed Jan 20 00:06:48 2016 +0100
     3.2 +++ b/src/Pure/General/symbol_pos.ML	Wed Jan 20 14:32:56 2016 +0100
     3.3 @@ -180,15 +180,15 @@
     3.4    Scan.repeat1 (Scan.depend (fn (depth: int option) =>
     3.5      (case depth of
     3.6        SOME d =>
     3.7 -        $$ "\\<open>" >> pair (SOME (d + 1)) ||
     3.8 +        $$ Symbol.open_ >> pair (SOME (d + 1)) ||
     3.9            (if d > 0 then
    3.10 -            Scan.one (fn (s, _) => s <> "\\<close>" andalso Symbol.not_eof s) >> pair depth ||
    3.11 -            $$ "\\<close>" >> pair (if d = 1 then NONE else SOME (d - 1))
    3.12 +            Scan.one (fn (s, _) => s <> Symbol.close andalso Symbol.not_eof s) >> pair depth ||
    3.13 +            $$ Symbol.close >> pair (if d = 1 then NONE else SOME (d - 1))
    3.14            else Scan.fail)
    3.15      | NONE => Scan.fail)));
    3.16  
    3.17  fun scan_cartouche err_prefix =
    3.18 -  Scan.ahead ($$ "\\<open>") |--
    3.19 +  Scan.ahead ($$ Symbol.open_) |--
    3.20      !!! (fn () => err_prefix ^ "unclosed text cartouche")
    3.21        (Scan.provide is_none (SOME 0) scan_cartouche_depth);
    3.22