editors/Viewer.py
changeset 1747 6046ffa2280f
parent 1745 f9d32913bad4
child 1749 d73b64672238
equal deleted inserted replaced
1746:45d6f5fba016 1747:6046ffa2280f
    63         parent.Append(help=help, id=id, kind=kind, text=text)
    63         parent.Append(help=help, id=id, kind=kind, text=text)
    64     else:
    64     else:
    65         parent.Append(helpString=help, id=id, kind=kind, item=text)
    65         parent.Append(helpString=help, id=id, kind=kind, item=text)
    66 
    66 
    67 if wx.Platform == '__WXMSW__':
    67 if wx.Platform == '__WXMSW__':
    68     faces = { 'times': 'Times New Roman',
    68     faces = {
    69               'mono':  'Courier New',
    69         'times': 'Times New Roman',
    70               'helv':  'Arial',
    70         'mono':  'Courier New',
    71               'other': 'Comic Sans MS',
    71         'helv':  'Arial',
    72               'size':  10,
    72         'other': 'Comic Sans MS',
    73              }
    73         'size':  10,
       
    74     }
    74 else:
    75 else:
    75     faces = { 'times': 'Times',
    76     faces = {
    76               'mono':  'Courier',
    77         'times': 'Times',
    77               'helv':  'Helvetica',
    78         'mono':  'Courier',
    78               'other': 'new century schoolbook',
    79         'helv':  'Helvetica',
    79               'size':  12,
    80         'other': 'new century schoolbook',
    80              }
    81         'size':  12,
       
    82     }
    81 
    83 
    82 if wx.Platform == '__WXMSW__':
    84 if wx.Platform == '__WXMSW__':
    83     MAX_ZOOMIN = 4
    85     MAX_ZOOMIN = 4
    84 else:
    86 else:
    85     MAX_ZOOMIN = 7
    87     MAX_ZOOMIN = 7