# HG changeset patch
# User wenzelm
# Date 1414789369 -3600
# Node ID b979c781c2dbf1df5f56bcc93efdfed0c709badb
# Parent  f8715e7c1be61bb03899ac5de03266f3ab5cc72e
discontinued obsolete \<^sync> marker;

diff -r f8715e7c1be6 -r b979c781c2db src/Pure/General/antiquote.ML
--- a/src/Pure/General/antiquote.ML	Fri Oct 31 21:48:40 2014 +0100
+++ b/src/Pure/General/antiquote.ML	Fri Oct 31 22:02:49 2014 +0100
@@ -49,12 +49,12 @@
 
 val scan_txt =
   Scan.repeat1 ($$$ "@" --| Scan.ahead (~$$ "{") ||
-    Scan.many1 (fn (s, _) => s <> "@" andalso Symbol.is_regular s)) >> flat;
+    Scan.many1 (fn (s, _) => s <> "@" andalso Symbol.not_eof s)) >> flat;
 
 val scan_antiq_body =
   Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 ||
   Scan.trace (Symbol_Pos.scan_cartouche err_prefix) >> #2 ||
-  Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single;
+  Scan.one (fn (s, _) => s <> "}" andalso Symbol.not_eof s) >> single;
 
 in
 
diff -r f8715e7c1be6 -r b979c781c2db src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Fri Oct 31 21:48:40 2014 +0100
+++ b/src/Pure/General/position.ML	Fri Oct 31 22:02:49 2014 +0100
@@ -90,7 +90,7 @@
 fun advance_count "\n" (i: int, j: int, k: int) =
       (if_valid i (i + 1), if_valid j (j + 1), k)
   | advance_count s (i, j, k) =
-      if Symbol.is_regular s then (i, if_valid j (j + 1), k)
+      if Symbol.not_eof s then (i, if_valid j (j + 1), k)
       else (i, j, k);
 
 fun invalid_count (i, j, _: int) =
diff -r f8715e7c1be6 -r b979c781c2db src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Fri Oct 31 21:48:40 2014 +0100
+++ b/src/Pure/General/symbol.ML	Fri Oct 31 22:02:49 2014 +0100
@@ -19,9 +19,6 @@
   val is_eof: symbol -> bool
   val not_eof: symbol -> bool
   val stopper: symbol Scan.stopper
-  val sync: symbol
-  val is_sync: symbol -> bool
-  val is_regular: symbol -> bool
   val is_malformed: symbol -> bool
   val malformed_msg: symbol -> string
   val is_ascii: symbol -> bool
@@ -119,12 +116,6 @@
 fun not_eof s = s <> eof;
 val stopper = Scan.stopper (K eof) is_eof;
 
-(*Proof General legacy*)
-val sync = "\\<^sync>";
-fun is_sync s = s = sync;
-
-fun is_regular s = not_eof s andalso s <> sync;
-
 fun is_malformed s =
   String.isPrefix "\\<" s andalso not (String.isSuffix ">" s)
   orelse s = "\\<>" orelse s = "\\<^>";
diff -r f8715e7c1be6 -r b979c781c2db src/Pure/General/symbol_pos.ML
--- a/src/Pure/General/symbol_pos.ML	Fri Oct 31 21:48:40 2014 +0100
+++ b/src/Pure/General/symbol_pos.ML	Fri Oct 31 22:02:49 2014 +0100
@@ -111,7 +111,7 @@
 fun scan_str q err_prefix =
   $$$ "\\" |-- !!! (fn () => err_prefix ^ "bad escape character in string")
     ($$$ q || $$$ "\\" || char_code) ||
-  Scan.one (fn (s, _) => s <> q andalso s <> "\\" andalso Symbol.is_regular s) >> single;
+  Scan.one (fn (s, _) => s <> q andalso s <> "\\" andalso Symbol.not_eof s) >> single;
 
 fun scan_strs q err_prefix =
   Scan.ahead ($$ q) |--
@@ -164,7 +164,7 @@
   Scan.repeat1 (Scan.depend (fn (d: int) =>
     $$ "\\<open>" >> pair (d + 1) ||
       (if d > 0 then
-        Scan.one (fn (s, _) => s <> "\\<close>" andalso Symbol.is_regular s) >> pair d ||
+        Scan.one (fn (s, _) => s <> "\\<close>" andalso Symbol.not_eof s) >> pair d ||
         $$ "\\<close>" >> pair (d - 1)
       else Scan.fail)));
 
@@ -198,7 +198,7 @@
   Scan.depend (fn (d: int) => $$$ "(" @@@ $$$ "*" >> pair (d + 1)) ||
   Scan.depend (fn 0 => Scan.fail | d => $$$ "*" @@@ $$$ ")" >> pair (d - 1)) ||
   Scan.lift ($$$ "*" --| Scan.ahead (~$$$ ")")) ||
-  Scan.lift (Scan.one (fn (s, _) => s <> "*" andalso Symbol.is_regular s)) >> single;
+  Scan.lift (Scan.one (fn (s, _) => s <> "*" andalso Symbol.not_eof s)) >> single;
 
 val scan_cmts = Scan.pass 0 (Scan.repeat scan_cmt >> flat);
 
diff -r f8715e7c1be6 -r b979c781c2db src/Pure/General/url.ML
--- a/src/Pure/General/url.ML	Fri Oct 31 21:48:40 2014 +0100
+++ b/src/Pure/General/url.ML	Fri Oct 31 22:02:49 2014 +0100
@@ -54,11 +54,11 @@
 local
 
 val scan_host =
-  (Scan.many1 (fn s => s <> "/" andalso Symbol.is_regular s) >> implode) --|
+  (Scan.many1 (fn s => s <> "/" andalso Symbol.not_eof s) >> implode) --|
   Scan.ahead ($$ "/" || Scan.one Symbol.is_eof);
 
-val scan_path = Scan.many Symbol.is_regular >> (Path.explode o implode);
-val scan_path_root = Scan.many Symbol.is_regular >> (Path.explode o implode o cons "/");
+val scan_path = Scan.many Symbol.not_eof >> (Path.explode o implode);
+val scan_path_root = Scan.many Symbol.not_eof >> (Path.explode o implode o cons "/");
 
 val scan_url =
   Scan.unless (Scan.this_string "file:" ||
diff -r f8715e7c1be6 -r b979c781c2db src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Fri Oct 31 21:48:40 2014 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Fri Oct 31 22:02:49 2014 +0100
@@ -75,9 +75,7 @@
 local
 
 fun terminate false = Scan.succeed ()
-  | terminate true =
-      Parse.group (fn () => "end of input")
-        (Scan.option Parse.sync -- Parse.semicolon >> K ());
+  | terminate true = Parse.group (fn () => "end of input") (Parse.semicolon >> K ());
 
 fun body cmd (name, _) =
   (case cmd name of
@@ -91,7 +89,6 @@
 
 fun parse_command do_terminate cmd =
   Parse.semicolon >> K NONE ||
-  Parse.sync >> K NONE ||
   (Parse.position Parse.command :-- body cmd) --| terminate do_terminate
     >> (fn ((name, pos), (int_only, f)) =>
       SOME (Toplevel.empty |> Toplevel.name name |> Toplevel.position pos |>
@@ -234,8 +231,7 @@
 
 fun toplevel_source term do_recover cmd src =
   let
-    val no_terminator =
-      Scan.unless Parse.semicolon (Scan.one (Token.not_sync andf Token.not_eof));
+    val no_terminator = Scan.unless Parse.semicolon (Scan.one Token.not_eof);
     fun recover int = (int, fn _ => Scan.repeat no_terminator >> K [NONE]);
   in
     src
diff -r f8715e7c1be6 -r b979c781c2db src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Fri Oct 31 21:48:40 2014 +0100
+++ b/src/Pure/Isar/parse.ML	Fri Oct 31 22:02:49 2014 +0100
@@ -32,7 +32,6 @@
   val alt_string: string parser
   val verbatim: string parser
   val cartouche: string parser
-  val sync: string parser
   val eof: string parser
   val command_name: string -> string parser
   val keyword_with: (string -> bool) -> string parser
@@ -196,7 +195,6 @@
 val alt_string = kind Token.AltString;
 val verbatim = kind Token.Verbatim;
 val cartouche = kind Token.Cartouche;
-val sync = kind Token.Sync;
 val eof = kind Token.EOF;
 
 fun command_name x =
diff -r f8715e7c1be6 -r b979c781c2db src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Fri Oct 31 21:48:40 2014 +0100
+++ b/src/Pure/Isar/token.ML	Fri Oct 31 22:02:49 2014 +0100
@@ -9,7 +9,7 @@
   datatype kind =
     Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
     Nat | Float | String | AltString | Verbatim | Cartouche | Space | Comment | InternalValue |
-    Error of string | Sync | EOF
+    Error of string | EOF
   val str_of_kind: kind -> string
   type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T}
   type T
@@ -35,7 +35,6 @@
   val eof: T
   val is_eof: T -> bool
   val not_eof: T -> bool
-  val not_sync: T -> bool
   val stopper: T Scan.stopper
   val kind_of: T -> kind
   val is_kind: kind -> T -> bool
@@ -104,7 +103,7 @@
 datatype kind =
   Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
   Nat | Float | String | AltString | Verbatim | Cartouche | Space | Comment | InternalValue |
-  Error of string | Sync | EOF;
+  Error of string | EOF;
 
 val str_of_kind =
  fn Command => "command"
@@ -125,7 +124,6 @@
   | Comment => "comment text"
   | InternalValue => "internal value"
   | Error _ => "bad input"
-  | Sync => "sync marker"
   | EOF => "end-of-input";
 
 val delimited_kind = member (op =) [String, AltString, Verbatim, Cartouche, Comment];
@@ -211,9 +209,6 @@
 
 val not_eof = not o is_eof;
 
-fun not_sync (Token (_, (Sync, _), _)) = false
-  | not_sync _ = true;
-
 val stopper =
   Scan.stopper (fn [] => eof | toks => mk_eof (end_pos_of (List.last toks))) is_eof;
 
@@ -305,7 +300,6 @@
   | Comment       => (Markup.comment, "")
   | InternalValue => (Markup.empty, "")
   | Error msg     => (Markup.bad, msg)
-  | Sync          => (Markup.control, "")
   | EOF           => (Markup.control, "");
 
 in
@@ -339,7 +333,6 @@
   | Verbatim => enclose "{*" "*}" x
   | Cartouche => cartouche x
   | Comment => enclose "(*" "*)" x
-  | Sync => ""
   | EOF => ""
   | _ => x);
 
@@ -493,7 +486,7 @@
 
 val scan_verb =
   $$$ "*" --| Scan.ahead (~$$ "}") ||
-  Scan.one (fn (s, _) => s <> "*" andalso Symbol.is_regular s) >> single;
+  Scan.one (fn (s, _) => s <> "*" andalso Symbol.not_eof s) >> single;
 
 val scan_verbatim =
   Scan.ahead ($$ "{" -- $$ "*") |--
@@ -549,7 +542,6 @@
     scan_cartouche >> token_range Cartouche ||
     scan_comment >> token_range Comment ||
     scan_space >> token Space ||
-    Scan.one (Symbol.is_sync o Symbol_Pos.symbol) >> (token Sync o single) ||
     (Scan.max token_leq
       (Scan.max token_leq
         (Scan.literal lex2 >> pair Command)
@@ -569,7 +561,7 @@
     recover_verbatim ||
     Symbol_Pos.recover_cartouche ||
     Symbol_Pos.recover_comment ||
-    Scan.one (Symbol.is_regular o Symbol_Pos.symbol) >> single)
+    Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> single)
   >> (single o token (Error msg));
 
 in
diff -r f8715e7c1be6 -r b979c781c2db src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Fri Oct 31 21:48:40 2014 +0100
+++ b/src/Pure/ML/ml_lex.ML	Fri Oct 31 22:02:49 2014 +0100
@@ -236,7 +236,7 @@
     Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) >> (fn ((a, b), c) => [a, b, c]);
 
 val scan_str =
-  Scan.one (fn (s, _) => Symbol.is_regular s andalso s <> "\"" andalso s <> "\\" andalso
+  Scan.one (fn (s, _) => Symbol.not_eof s andalso s <> "\"" andalso s <> "\\" andalso
     (not (Symbol.is_char s) orelse Symbol.is_printable s)) >> single ||
   $$$ "\\" @@@ !!! "bad escape character in string" scan_escape;
 
diff -r f8715e7c1be6 -r b979c781c2db src/Pure/PIDE/xml.ML
--- a/src/Pure/PIDE/xml.ML	Fri Oct 31 21:48:40 2014 +0100
+++ b/src/Pure/PIDE/xml.ML	Fri Oct 31 22:02:49 2014 +0100
@@ -192,8 +192,8 @@
 
 val blanks = Scan.many Symbol.is_blank;
 val special = $$ "&" ^^ (parse_name >> implode) ^^ $$ ";" >> decode;
-val regular = Scan.one Symbol.is_regular;
-fun regular_except x = Scan.one (fn c => Symbol.is_regular c andalso c <> x);
+val regular = Scan.one Symbol.not_eof;
+fun regular_except x = Scan.one (fn c => Symbol.not_eof c andalso c <> x);
 
 val parse_chars = Scan.repeat1 (special || regular_except "<") >> implode;
 
diff -r f8715e7c1be6 -r b979c781c2db src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Fri Oct 31 21:48:40 2014 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Fri Oct 31 22:02:49 2014 +0100
@@ -230,7 +230,7 @@
 val scan_chr =
   $$ "\\" |-- $$$ "'" ||
   Scan.one
-    ((fn s => s <> "\\" andalso s <> "'" andalso Symbol.is_regular s) o
+    ((fn s => s <> "\\" andalso s <> "'" andalso Symbol.not_eof s) o
       Symbol_Pos.symbol) >> single ||
   $$$ "'" --| Scan.ahead (~$$ "'");
 
@@ -339,7 +339,7 @@
     val scan =
       $$ "?" |-- scan_indexname --| Scan.ahead (Scan.one Symbol_Pos.is_eof)
         >> Syntax.var ||
-      Scan.many (Symbol.is_regular o Symbol_Pos.symbol)
+      Scan.many (Symbol.not_eof o Symbol_Pos.symbol)
         >> (Syntax.free o implode o map Symbol_Pos.symbol);
   in the (Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode (str, Position.none))) end;
 
diff -r f8715e7c1be6 -r b979c781c2db src/Pure/Syntax/syntax_ext.ML
--- a/src/Pure/Syntax/syntax_ext.ML	Fri Oct 31 21:48:40 2014 +0100
+++ b/src/Pure/Syntax/syntax_ext.ML	Fri Oct 31 22:02:49 2014 +0100
@@ -143,8 +143,8 @@
 val is_meta = member (op =) ["(", ")", "/", "_", "\\<index>"];
 
 val scan_delim_char =
-  $$ "'" |-- Scan.one ((not o Symbol.is_blank) andf Symbol.is_regular) ||
-  Scan.one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.is_regular);
+  $$ "'" |-- Scan.one ((not o Symbol.is_blank) andf Symbol.not_eof) ||
+  Scan.one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.not_eof);
 
 fun read_int ["0", "0"] = ~1
   | read_int cs = #1 (Library.read_int cs);
diff -r f8715e7c1be6 -r b979c781c2db src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Fri Oct 31 21:48:40 2014 +0100
+++ b/src/Tools/Code/code_printer.ML	Fri Oct 31 22:02:49 2014 +0100
@@ -373,7 +373,7 @@
 
 fun read_mixfix s =
   let
-    val sym_any = Scan.one Symbol.is_regular;
+    val sym_any = Scan.one Symbol.not_eof;
     val parse = Scan.optional ($$ "!" >> K NOBR) BR -- Scan.repeat (
          ($$ "(" -- $$ "_" -- $$ ")" >> K (Arg NOBR))
       || ($$ "_" >> K (Arg BR))