2013-06-26 01:28:25 +00:00
|
|
|
# coding: utf-8
|
2013-08-31 15:03:37 +00: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-26 01:28:25 +00:00
|
|
|
|
2013-06-21 04:58:35 +00:00
|
|
|
import os
|
|
|
|
import sys
|
2013-09-02 15:41:50 +00:00
|
|
|
|
2013-06-21 04:58:35 +00:00
|
|
|
import preprocessor
|
|
|
|
|
2013-12-08 22:05:28 +00:00
|
|
|
def preprocess_queue(filenames=sys.argv[1:]):
|
2013-08-31 16:04:27 +00:00
|
|
|
|
2013-12-08 22:05:28 +00:00
|
|
|
stdin = sys.stdin
|
2013-08-31 16:07:49 +00:00
|
|
|
stdout = sys.stdout
|
|
|
|
|
2013-12-08 22:05:28 +00:00
|
|
|
processor = preprocessor.setup_processor()
|
|
|
|
|
|
|
|
for source in filenames:
|
2013-06-26 03:25:50 +00:00
|
|
|
dest = os.path.splitext(source)[0] + '.tx'
|
|
|
|
sys.stdin = open(source, 'r')
|
|
|
|
sys.stdout = open(dest, 'w')
|
2013-12-08 22:05:28 +00:00
|
|
|
processor.preprocess()
|
2013-08-31 16:04:27 +00:00
|
|
|
|
2013-12-08 22:05:28 +00:00
|
|
|
processor.update_globals()
|
|
|
|
|
|
|
|
sys.stdin = stdin
|
2013-08-31 16:07:49 +00:00
|
|
|
sys.stdout = stdout
|
|
|
|
|
2013-12-08 22:05:28 +00: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 16:04:27 +00:00
|
|
|
if __name__ == '__main__':
|
|
|
|
main()
|