diff -r 0364007b4bb3 -r 6e6eb8d92377 src/Pure/General/symbol.ML --- a/src/Pure/General/symbol.ML Wed Jun 30 09:47:16 1999 +0200 +++ b/src/Pure/General/symbol.ML Wed Jun 30 12:22:31 1999 +0200 @@ -9,6 +9,9 @@ sig type symbol val space: symbol + val sync: symbol + val is_sync: symbol -> bool + val not_sync: symbol -> bool val eof: symbol val is_eof: symbol -> bool val not_eof: symbol -> bool @@ -55,11 +58,15 @@ type symbol = string; val space = " "; +val sync = "\\<^sync>"; val eof = ""; (* kinds *) +fun is_sync s = s = sync; +fun not_sync s = s <> sync; + fun is_eof s = s = eof; fun not_eof s = s <> eof; val stopper = (eof, is_eof);