On Wed, Aug 22, 2001 at 06:32:55PM +0200, Andre Poenitz wrote:
>
> Next try.
Here is an updated version of Andre's patch.
This version allow to view on screen (almost) all AMS symbols.
font4.diff.gz
#!/usr/bin/python
import sys,string,re
def is_prefix(a, b):
return a[:len(b)] == b
def get_code(code):
if code < 10:
return code+161
elif code < 32:
return code+163
else:
return code
font_names = {}
symbols = {}
def process(file):
fh = open(file)
lines = fh.readlines()
fh.close()
n = len(lines)
for i in xrange(n):
line = lines[i]
next_line = ""
if i+1 < n:
next_line = lines[i+1]
# some entries are spread over two lines so we joint the next line
# to the current one, removing any comments
line = string.split(line,'%')[0]+string.split(next_line,'%')[0]
mo =
re.match(r'\s*\\DeclareSymbolFont\s*\{(.*?)\}\s*\{(.*?)\}\s*\{(.*?)\}.*', line)
if mo != None:
font_names[mo.group(1)] = mo.group(3)
mo =
re.match(r'\s*\\DeclareMath(Symbol|Delimiter)\s*\{?\\(.*?)\}?\s*\{(.*?)\}\s*\{(.*?)\}\s*\{"(.*?)\}.*',
line)
if mo != None:
symbol = mo.group(2)
mo2 = re.match(r'\s*\\def\\(.*?)\{', next_line)
if mo2 != None and is_prefix(symbol,mo2.group(1)):
sys.stderr.write("%s -> %s\n" % (symbol, mo2.group(1)))
symbol = mo2.group(1)
font = mo.group(4)
if font_names.has_key(font):
font = font_names[font]
code = get_code(string.atoi(mo.group(5),16))
if symbols.has_key(symbol):
sys.stderr.write(symbol+ " exists\n")
else:
symbols[symbol] = 1
print "%-18s %-4s %3d" % (symbol,font,code)
for file in sys.argv[1:]:
print "# Generated from " + file + "\n"
process(file)
print
