discontinued obsolete \<^sync> marker;
authorwenzelm
Fri Oct 31 22:02:49 2014 +0100 (2014-10-31)
changeset 58854b979c781c2db
parent 58853 f8715e7c1be6
child 58855 2885e2eaa0fb
discontinued obsolete \<^sync> marker;
src/Pure/General/antiquote.ML
src/Pure/General/position.ML
src/Pure/General/symbol.ML
src/Pure/General/symbol_pos.ML
src/Pure/General/url.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/parse.ML
src/Pure/Isar/token.ML
src/Pure/ML/ml_lex.ML
src/Pure/PIDE/xml.ML
src/Pure/Syntax/lexicon.ML
src/Pure/Syntax/syntax_ext.ML
src/Tools/Code/code_printer.ML
     1.1 --- a/src/Pure/General/antiquote.ML	Fri Oct 31 21:48:40 2014 +0100
     1.2 +++ b/src/Pure/General/antiquote.ML	Fri Oct 31 22:02:49 2014 +0100
     1.3 @@ -49,12 +49,12 @@
     1.4  
     1.5  val scan_txt =
     1.6    Scan.repeat1 ($$$ "@" --| Scan.ahead (~$$ "{") ||
     1.7 -    Scan.many1 (fn (s, _) => s <> "@" andalso Symbol.is_regular s)) >> flat;
     1.8 +    Scan.many1 (fn (s, _) => s <> "@" andalso Symbol.not_eof s)) >> flat;
     1.9  
    1.10  val scan_antiq_body =
    1.11    Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 ||
    1.12    Scan.trace (Symbol_Pos.scan_cartouche err_prefix) >> #2 ||
    1.13 -  Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single;
    1.14 +  Scan.one (fn (s, _) => s <> "}" andalso Symbol.not_eof s) >> single;
    1.15  
    1.16  in
    1.17  
     2.1 --- a/src/Pure/General/position.ML	Fri Oct 31 21:48:40 2014 +0100
     2.2 +++ b/src/Pure/General/position.ML	Fri Oct 31 22:02:49 2014 +0100
     2.3 @@ -90,7 +90,7 @@
     2.4  fun advance_count "\n" (i: int, j: int, k: int) =
     2.5        (if_valid i (i + 1), if_valid j (j + 1), k)
     2.6    | advance_count s (i, j, k) =
     2.7 -      if Symbol.is_regular s then (i, if_valid j (j + 1), k)
     2.8 +      if Symbol.not_eof s then (i, if_valid j (j + 1), k)
     2.9        else (i, j, k);
    2.10  
    2.11  fun invalid_count (i, j, _: int) =
     3.1 --- a/src/Pure/General/symbol.ML	Fri Oct 31 21:48:40 2014 +0100
     3.2 +++ b/src/Pure/General/symbol.ML	Fri Oct 31 22:02:49 2014 +0100
     3.3 @@ -19,9 +19,6 @@
     3.4    val is_eof: symbol -> bool
     3.5    val not_eof: symbol -> bool
     3.6    val stopper: symbol Scan.stopper
     3.7 -  val sync: symbol
     3.8 -  val is_sync: symbol -> bool
     3.9 -  val is_regular: symbol -> bool
    3.10    val is_malformed: symbol -> bool
    3.11    val malformed_msg: symbol -> string
    3.12    val is_ascii: symbol -> bool
    3.13 @@ -119,12 +116,6 @@
    3.14  fun not_eof s = s <> eof;
    3.15  val stopper = Scan.stopper (K eof) is_eof;
    3.16  
    3.17 -(*Proof General legacy*)
    3.18 -val sync = "\\<^sync>";
    3.19 -fun is_sync s = s = sync;
    3.20 -
    3.21 -fun is_regular s = not_eof s andalso s <> sync;
    3.22 -
    3.23  fun is_malformed s =
    3.24    String.isPrefix "\\<" s andalso not (String.isSuffix ">" s)
    3.25    orelse s = "\\<>" orelse s = "\\<^>";
     4.1 --- a/src/Pure/General/symbol_pos.ML	Fri Oct 31 21:48:40 2014 +0100
     4.2 +++ b/src/Pure/General/symbol_pos.ML	Fri Oct 31 22:02:49 2014 +0100
     4.3 @@ -111,7 +111,7 @@
     4.4  fun scan_str q err_prefix =
     4.5    $$$ "\\" |-- !!! (fn () => err_prefix ^ "bad escape character in string")
     4.6      ($$$ q || $$$ "\\" || char_code) ||
     4.7 -  Scan.one (fn (s, _) => s <> q andalso s <> "\\" andalso Symbol.is_regular s) >> single;
     4.8 +  Scan.one (fn (s, _) => s <> q andalso s <> "\\" andalso Symbol.not_eof s) >> single;
     4.9  
    4.10  fun scan_strs q err_prefix =
    4.11    Scan.ahead ($$ q) |--
    4.12 @@ -164,7 +164,7 @@
    4.13    Scan.repeat1 (Scan.depend (fn (d: int) =>
    4.14      $$ "\\<open>" >> pair (d + 1) ||
    4.15        (if d > 0 then
    4.16 -        Scan.one (fn (s, _) => s <> "\\<close>" andalso Symbol.is_regular s) >> pair d ||
    4.17 +        Scan.one (fn (s, _) => s <> "\\<close>" andalso Symbol.not_eof s) >> pair d ||
    4.18          $$ "\\<close>" >> pair (d - 1)
    4.19        else Scan.fail)));
    4.20  
    4.21 @@ -198,7 +198,7 @@
    4.22    Scan.depend (fn (d: int) => $$$ "(" @@@ $$$ "*" >> pair (d + 1)) ||
    4.23    Scan.depend (fn 0 => Scan.fail | d => $$$ "*" @@@ $$$ ")" >> pair (d - 1)) ||
    4.24    Scan.lift ($$$ "*" --| Scan.ahead (~$$$ ")")) ||
    4.25 -  Scan.lift (Scan.one (fn (s, _) => s <> "*" andalso Symbol.is_regular s)) >> single;
    4.26 +  Scan.lift (Scan.one (fn (s, _) => s <> "*" andalso Symbol.not_eof s)) >> single;
    4.27  
    4.28  val scan_cmts = Scan.pass 0 (Scan.repeat scan_cmt >> flat);
    4.29  
     5.1 --- a/src/Pure/General/url.ML	Fri Oct 31 21:48:40 2014 +0100
     5.2 +++ b/src/Pure/General/url.ML	Fri Oct 31 22:02:49 2014 +0100
     5.3 @@ -54,11 +54,11 @@
     5.4  local
     5.5  
     5.6  val scan_host =
     5.7 -  (Scan.many1 (fn s => s <> "/" andalso Symbol.is_regular s) >> implode) --|
     5.8 +  (Scan.many1 (fn s => s <> "/" andalso Symbol.not_eof s) >> implode) --|
     5.9    Scan.ahead ($$ "/" || Scan.one Symbol.is_eof);
    5.10  
    5.11 -val scan_path = Scan.many Symbol.is_regular >> (Path.explode o implode);
    5.12 -val scan_path_root = Scan.many Symbol.is_regular >> (Path.explode o implode o cons "/");
    5.13 +val scan_path = Scan.many Symbol.not_eof >> (Path.explode o implode);
    5.14 +val scan_path_root = Scan.many Symbol.not_eof >> (Path.explode o implode o cons "/");
    5.15  
    5.16  val scan_url =
    5.17    Scan.unless (Scan.this_string "file:" ||
     6.1 --- a/src/Pure/Isar/outer_syntax.ML	Fri Oct 31 21:48:40 2014 +0100
     6.2 +++ b/src/Pure/Isar/outer_syntax.ML	Fri Oct 31 22:02:49 2014 +0100
     6.3 @@ -75,9 +75,7 @@
     6.4  local
     6.5  
     6.6  fun terminate false = Scan.succeed ()
     6.7 -  | terminate true =
     6.8 -      Parse.group (fn () => "end of input")
     6.9 -        (Scan.option Parse.sync -- Parse.semicolon >> K ());
    6.10 +  | terminate true = Parse.group (fn () => "end of input") (Parse.semicolon >> K ());
    6.11  
    6.12  fun body cmd (name, _) =
    6.13    (case cmd name of
    6.14 @@ -91,7 +89,6 @@
    6.15  
    6.16  fun parse_command do_terminate cmd =
    6.17    Parse.semicolon >> K NONE ||
    6.18 -  Parse.sync >> K NONE ||
    6.19    (Parse.position Parse.command :-- body cmd) --| terminate do_terminate
    6.20      >> (fn ((name, pos), (int_only, f)) =>
    6.21        SOME (Toplevel.empty |> Toplevel.name name |> Toplevel.position pos |>
    6.22 @@ -234,8 +231,7 @@
    6.23  
    6.24  fun toplevel_source term do_recover cmd src =
    6.25    let
    6.26 -    val no_terminator =
    6.27 -      Scan.unless Parse.semicolon (Scan.one (Token.not_sync andf Token.not_eof));
    6.28 +    val no_terminator = Scan.unless Parse.semicolon (Scan.one Token.not_eof);
    6.29      fun recover int = (int, fn _ => Scan.repeat no_terminator >> K [NONE]);
    6.30    in
    6.31      src
     7.1 --- a/src/Pure/Isar/parse.ML	Fri Oct 31 21:48:40 2014 +0100
     7.2 +++ b/src/Pure/Isar/parse.ML	Fri Oct 31 22:02:49 2014 +0100
     7.3 @@ -32,7 +32,6 @@
     7.4    val alt_string: string parser
     7.5    val verbatim: string parser
     7.6    val cartouche: string parser
     7.7 -  val sync: string parser
     7.8    val eof: string parser
     7.9    val command_name: string -> string parser
    7.10    val keyword_with: (string -> bool) -> string parser
    7.11 @@ -196,7 +195,6 @@
    7.12  val alt_string = kind Token.AltString;
    7.13  val verbatim = kind Token.Verbatim;
    7.14  val cartouche = kind Token.Cartouche;
    7.15 -val sync = kind Token.Sync;
    7.16  val eof = kind Token.EOF;
    7.17  
    7.18  fun command_name x =
     8.1 --- a/src/Pure/Isar/token.ML	Fri Oct 31 21:48:40 2014 +0100
     8.2 +++ b/src/Pure/Isar/token.ML	Fri Oct 31 22:02:49 2014 +0100
     8.3 @@ -9,7 +9,7 @@
     8.4    datatype kind =
     8.5      Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
     8.6      Nat | Float | String | AltString | Verbatim | Cartouche | Space | Comment | InternalValue |
     8.7 -    Error of string | Sync | EOF
     8.8 +    Error of string | EOF
     8.9    val str_of_kind: kind -> string
    8.10    type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T}
    8.11    type T
    8.12 @@ -35,7 +35,6 @@
    8.13    val eof: T
    8.14    val is_eof: T -> bool
    8.15    val not_eof: T -> bool
    8.16 -  val not_sync: T -> bool
    8.17    val stopper: T Scan.stopper
    8.18    val kind_of: T -> kind
    8.19    val is_kind: kind -> T -> bool
    8.20 @@ -104,7 +103,7 @@
    8.21  datatype kind =
    8.22    Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
    8.23    Nat | Float | String | AltString | Verbatim | Cartouche | Space | Comment | InternalValue |
    8.24 -  Error of string | Sync | EOF;
    8.25 +  Error of string | EOF;
    8.26  
    8.27  val str_of_kind =
    8.28   fn Command => "command"
    8.29 @@ -125,7 +124,6 @@
    8.30    | Comment => "comment text"
    8.31    | InternalValue => "internal value"
    8.32    | Error _ => "bad input"
    8.33 -  | Sync => "sync marker"
    8.34    | EOF => "end-of-input";
    8.35  
    8.36  val delimited_kind = member (op =) [String, AltString, Verbatim, Cartouche, Comment];
    8.37 @@ -211,9 +209,6 @@
    8.38  
    8.39  val not_eof = not o is_eof;
    8.40  
    8.41 -fun not_sync (Token (_, (Sync, _), _)) = false
    8.42 -  | not_sync _ = true;
    8.43 -
    8.44  val stopper =
    8.45    Scan.stopper (fn [] => eof | toks => mk_eof (end_pos_of (List.last toks))) is_eof;
    8.46  
    8.47 @@ -305,7 +300,6 @@
    8.48    | Comment       => (Markup.comment, "")
    8.49    | InternalValue => (Markup.empty, "")
    8.50    | Error msg     => (Markup.bad, msg)
    8.51 -  | Sync          => (Markup.control, "")
    8.52    | EOF           => (Markup.control, "");
    8.53  
    8.54  in
    8.55 @@ -339,7 +333,6 @@
    8.56    | Verbatim => enclose "{*" "*}" x
    8.57    | Cartouche => cartouche x
    8.58    | Comment => enclose "(*" "*)" x
    8.59 -  | Sync => ""
    8.60    | EOF => ""
    8.61    | _ => x);
    8.62  
    8.63 @@ -493,7 +486,7 @@
    8.64  
    8.65  val scan_verb =
    8.66    $$$ "*" --| Scan.ahead (~$$ "}") ||
    8.67 -  Scan.one (fn (s, _) => s <> "*" andalso Symbol.is_regular s) >> single;
    8.68 +  Scan.one (fn (s, _) => s <> "*" andalso Symbol.not_eof s) >> single;
    8.69  
    8.70  val scan_verbatim =
    8.71    Scan.ahead ($$ "{" -- $$ "*") |--
    8.72 @@ -549,7 +542,6 @@
    8.73      scan_cartouche >> token_range Cartouche ||
    8.74      scan_comment >> token_range Comment ||
    8.75      scan_space >> token Space ||
    8.76 -    Scan.one (Symbol.is_sync o Symbol_Pos.symbol) >> (token Sync o single) ||
    8.77      (Scan.max token_leq
    8.78        (Scan.max token_leq
    8.79          (Scan.literal lex2 >> pair Command)
    8.80 @@ -569,7 +561,7 @@
    8.81      recover_verbatim ||
    8.82      Symbol_Pos.recover_cartouche ||
    8.83      Symbol_Pos.recover_comment ||
    8.84 -    Scan.one (Symbol.is_regular o Symbol_Pos.symbol) >> single)
    8.85 +    Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> single)
    8.86    >> (single o token (Error msg));
    8.87  
    8.88  in
     9.1 --- a/src/Pure/ML/ml_lex.ML	Fri Oct 31 21:48:40 2014 +0100
     9.2 +++ b/src/Pure/ML/ml_lex.ML	Fri Oct 31 22:02:49 2014 +0100
     9.3 @@ -236,7 +236,7 @@
     9.4      Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) >> (fn ((a, b), c) => [a, b, c]);
     9.5  
     9.6  val scan_str =
     9.7 -  Scan.one (fn (s, _) => Symbol.is_regular s andalso s <> "\"" andalso s <> "\\" andalso
     9.8 +  Scan.one (fn (s, _) => Symbol.not_eof s andalso s <> "\"" andalso s <> "\\" andalso
     9.9      (not (Symbol.is_char s) orelse Symbol.is_printable s)) >> single ||
    9.10    $$$ "\\" @@@ !!! "bad escape character in string" scan_escape;
    9.11  
    10.1 --- a/src/Pure/PIDE/xml.ML	Fri Oct 31 21:48:40 2014 +0100
    10.2 +++ b/src/Pure/PIDE/xml.ML	Fri Oct 31 22:02:49 2014 +0100
    10.3 @@ -192,8 +192,8 @@
    10.4  
    10.5  val blanks = Scan.many Symbol.is_blank;
    10.6  val special = $$ "&" ^^ (parse_name >> implode) ^^ $$ ";" >> decode;
    10.7 -val regular = Scan.one Symbol.is_regular;
    10.8 -fun regular_except x = Scan.one (fn c => Symbol.is_regular c andalso c <> x);
    10.9 +val regular = Scan.one Symbol.not_eof;
   10.10 +fun regular_except x = Scan.one (fn c => Symbol.not_eof c andalso c <> x);
   10.11  
   10.12  val parse_chars = Scan.repeat1 (special || regular_except "<") >> implode;
   10.13  
    11.1 --- a/src/Pure/Syntax/lexicon.ML	Fri Oct 31 21:48:40 2014 +0100
    11.2 +++ b/src/Pure/Syntax/lexicon.ML	Fri Oct 31 22:02:49 2014 +0100
    11.3 @@ -230,7 +230,7 @@
    11.4  val scan_chr =
    11.5    $$ "\\" |-- $$$ "'" ||
    11.6    Scan.one
    11.7 -    ((fn s => s <> "\\" andalso s <> "'" andalso Symbol.is_regular s) o
    11.8 +    ((fn s => s <> "\\" andalso s <> "'" andalso Symbol.not_eof s) o
    11.9        Symbol_Pos.symbol) >> single ||
   11.10    $$$ "'" --| Scan.ahead (~$$ "'");
   11.11  
   11.12 @@ -339,7 +339,7 @@
   11.13      val scan =
   11.14        $$ "?" |-- scan_indexname --| Scan.ahead (Scan.one Symbol_Pos.is_eof)
   11.15          >> Syntax.var ||
   11.16 -      Scan.many (Symbol.is_regular o Symbol_Pos.symbol)
   11.17 +      Scan.many (Symbol.not_eof o Symbol_Pos.symbol)
   11.18          >> (Syntax.free o implode o map Symbol_Pos.symbol);
   11.19    in the (Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode (str, Position.none))) end;
   11.20  
    12.1 --- a/src/Pure/Syntax/syntax_ext.ML	Fri Oct 31 21:48:40 2014 +0100
    12.2 +++ b/src/Pure/Syntax/syntax_ext.ML	Fri Oct 31 22:02:49 2014 +0100
    12.3 @@ -143,8 +143,8 @@
    12.4  val is_meta = member (op =) ["(", ")", "/", "_", "\\<index>"];
    12.5  
    12.6  val scan_delim_char =
    12.7 -  $$ "'" |-- Scan.one ((not o Symbol.is_blank) andf Symbol.is_regular) ||
    12.8 -  Scan.one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.is_regular);
    12.9 +  $$ "'" |-- Scan.one ((not o Symbol.is_blank) andf Symbol.not_eof) ||
   12.10 +  Scan.one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.not_eof);
   12.11  
   12.12  fun read_int ["0", "0"] = ~1
   12.13    | read_int cs = #1 (Library.read_int cs);
    13.1 --- a/src/Tools/Code/code_printer.ML	Fri Oct 31 21:48:40 2014 +0100
    13.2 +++ b/src/Tools/Code/code_printer.ML	Fri Oct 31 22:02:49 2014 +0100
    13.3 @@ -373,7 +373,7 @@
    13.4  
    13.5  fun read_mixfix s =
    13.6    let
    13.7 -    val sym_any = Scan.one Symbol.is_regular;
    13.8 +    val sym_any = Scan.one Symbol.not_eof;
    13.9      val parse = Scan.optional ($$ "!" >> K NOBR) BR -- Scan.repeat (
   13.10           ($$ "(" -- $$ "_" -- $$ ")" >> K (Arg NOBR))
   13.11        || ($$ "_" >> K (Arg BR))