equal
deleted
inserted
replaced
25 import wx |
25 import wx |
26 import wx.stc |
26 import wx.stc |
27 |
27 |
28 if wx.Platform == '__WXMSW__': |
28 if wx.Platform == '__WXMSW__': |
29 faces = { 'times': 'Times New Roman', |
29 faces = { 'times': 'Times New Roman', |
30 'mono' : 'Courier New', |
30 'mono': 'Courier New', |
31 'helv' : 'Arial', |
31 'helv': 'Arial', |
32 'other': 'Comic Sans MS', |
32 'other': 'Comic Sans MS', |
33 'size' : 10, |
33 'size': 10, |
34 } |
34 } |
35 else: |
35 else: |
36 faces = { 'times': 'Times', |
36 faces = { 'times': 'Times', |
37 'mono' : 'Courier', |
37 'mono': 'Courier', |
38 'helv' : 'Helvetica', |
38 'helv': 'Helvetica', |
39 'other': 'new century schoolbook', |
39 'other': 'new century schoolbook', |
40 'size' : 12, |
40 'size': 12, |
41 } |
41 } |
42 |
42 |
43 NAVIGATION_KEYS = [ |
43 NAVIGATION_KEYS = [ |
44 wx.WXK_END, |
44 wx.WXK_END, |
45 wx.WXK_HOME, |
45 wx.WXK_HOME, |