tok_to_bin.py

   1 #!/usr/bin/env python3
   2
   3 import os
   4 import sys
   5
   6 bin = []
   7 def byte(value):
   8   bin.append(value & 0xff)
   9 def word(value):
  10   bin.extend([value & 0xff, (value >> 8) & 0xff])
  11
  12 word(0)
  13 for line in sys.stdin:
  14   line = [ord(i) for i in line]
  15   assert line.pop() == 0xa
  16
  17   i = 0
  18   line_number = 0
  19   while i < len(line) and line[i] >= 0x30 and line[i] < 0x3a:
  20     line_number = line_number * 10 + (line[i] & 0xf)
  21     i += 1
  22   line = line[i:]
  23
  24   word(len(bin) + 4 + len(line) + 0x800)
  25   word(line_number)
  26   bin.extend(line)
  27   byte(0)
  28 bin[0] = len(bin) & 0xff
  29 bin[1] = (len(bin) >> 8) & 0xff
  30 word(0)
  31 assert os.write(sys.stdout.fileno(), bytes(bin)) == len(bin)