2013-06-25 18:28:25 -07:00
|
|
|
# coding: utf-8
|
2013-08-31 08:03:37 -07:00
|
|
|
"""
|
|
|
|
Starting a new python process to preprocess each source file creates too much
|
|
|
|
overhead. Instead, a list of files to preprocess is fed into a script run from
|
|
|
|
a single process.
|
|
|
|
"""
|
2013-06-25 18:28:25 -07:00
|
|
|
|
2013-06-20 21:58:35 -07:00
|
|
|
import os
|
|
|
|
import sys
|
2013-09-02 08:41:50 -07:00
|
|
|
|
2013-06-20 21:58:35 -07:00
|
|
|
import preprocessor
|
|
|
|
|
2013-12-08 14:05:28 -08:00
|
|
|
def preprocess_queue(filenames=sys.argv[1:]):
|
2013-08-31 09:04:27 -07:00
|
|
|
|
2013-12-08 14:05:28 -08:00
|
|
|
stdin = sys.stdin
|
2013-08-31 09:07:49 -07:00
|
|
|
stdout = sys.stdout
|
|
|
|
|
2013-12-08 14:05:28 -08:00
|
|
|
processor = preprocessor.setup_processor()
|
|
|
|
|
|
|
|
for source in filenames:
|
2013-06-25 20:25:50 -07:00
|
|
|
dest = os.path.splitext(source)[0] + '.tx'
|
|
|
|
sys.stdin = open(source, 'r')
|
|
|
|
sys.stdout = open(dest, 'w')
|
2013-12-08 14:05:28 -08:00
|
|
|
processor.preprocess()
|
2013-08-31 09:04:27 -07:00
|
|
|
|
2013-12-08 14:05:28 -08:00
|
|
|
sys.stdin = stdin
|
2013-08-31 09:07:49 -07:00
|
|
|
sys.stdout = stdout
|
|
|
|
|
2013-12-08 14:05:28 -08:00
|
|
|
def main():
|
|
|
|
filenames = list(set(sys.argv[1:]))
|
|
|
|
if filenames:
|
|
|
|
num_files = len(filenames)
|
|
|
|
s = '' if num_files == 1 else 's'
|
|
|
|
sys.stdout.write('Preprocessing {0} file{1}...\n'.format(num_files, s))
|
|
|
|
preprocess_queue(filenames)
|
|
|
|
|
2013-08-31 09:04:27 -07:00
|
|
|
if __name__ == '__main__':
|
|
|
|
main()
|