[nneonneo]

Yes, I'd be happy if you did so! I tried adding a reply but since I don't yet have a Mastodon account (hopefully soon to be resolved), I resorted to just posting here instead.

Here's the decode script I used to produce the table above:

  rom = open('exsb1.dat', 'rb').read()
  ptr =  0xf6
  for i in range(128, 256):
      out = bytearray([rom[ptr] - 0x80])
      while rom[ptr+1] < 0x80:
          out.append(rom[ptr+1])
          ptr += 1
      ptr += 1
      print(i, hex(i), bytes(out))

The format of the tokens packed into the BASIC ROM is quite simple: the first byte in each token is ORed with 0x80 and the tokens are concatenated without any other separators. Tokens end when the next byte has 0x80 set (indicating the start of the next token).