src/Pure/General/symbol.ML
changeset 6857 6e6eb8d92377
parent 6692 05c56f41e661
child 8230 6f8aa407bcf9
equal deleted inserted replaced
6856:0364007b4bb3 6857:6e6eb8d92377
     7 
     7 
     8 signature SYMBOL =
     8 signature SYMBOL =
     9 sig
     9 sig
    10   type symbol
    10   type symbol
    11   val space: symbol
    11   val space: symbol
       
    12   val sync: symbol
       
    13   val is_sync: symbol -> bool
       
    14   val not_sync: symbol -> bool
    12   val eof: symbol
    15   val eof: symbol
    13   val is_eof: symbol -> bool
    16   val is_eof: symbol -> bool
    14   val not_eof: symbol -> bool
    17   val not_eof: symbol -> bool
    15   val stopper: symbol * (symbol -> bool)
    18   val stopper: symbol * (symbol -> bool)
    16   val is_ascii: symbol -> bool
    19   val is_ascii: symbol -> bool
    53 *)
    56 *)
    54 
    57 
    55 type symbol = string;
    58 type symbol = string;
    56 
    59 
    57 val space = " ";
    60 val space = " ";
       
    61 val sync = "\\<^sync>";
    58 val eof = "";
    62 val eof = "";
    59 
    63 
    60 
    64 
    61 (* kinds *)
    65 (* kinds *)
       
    66 
       
    67 fun is_sync s = s = sync;
       
    68 fun not_sync s = s <> sync;
    62 
    69 
    63 fun is_eof s = s = eof;
    70 fun is_eof s = s = eof;
    64 fun not_eof s = s <> eof;
    71 fun not_eof s = s <> eof;
    65 val stopper = (eof, is_eof);
    72 val stopper = (eof, is_eof);
    66 
    73