equal
deleted
inserted
replaced
24 |
24 |
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 = { |
30 'mono': 'Courier New', |
30 'times': 'Times New Roman', |
31 'helv': 'Arial', |
31 'mono': 'Courier New', |
32 'other': 'Comic Sans MS', |
32 'helv': 'Arial', |
33 'size': 10, |
33 'other': 'Comic Sans MS', |
34 } |
34 'size': 10, |
|
35 } |
35 else: |
36 else: |
36 faces = { 'times': 'Times', |
37 faces = { |
37 'mono': 'Courier', |
38 'times': 'Times', |
38 'helv': 'Helvetica', |
39 'mono': 'Courier', |
39 'other': 'new century schoolbook', |
40 'helv': 'Helvetica', |
40 'size': 12, |
41 'other': 'new century schoolbook', |
41 } |
42 'size': 12, |
|
43 } |
42 |
44 |
43 NAVIGATION_KEYS = [ |
45 NAVIGATION_KEYS = [ |
44 wx.WXK_END, |
46 wx.WXK_END, |
45 wx.WXK_HOME, |
47 wx.WXK_HOME, |
46 wx.WXK_LEFT, |
48 wx.WXK_LEFT, |