--- a/Viewer.py Mon Jan 28 10:31:29 2008 +0100
+++ b/Viewer.py Mon Jan 28 10:48:16 2008 +0100
@@ -39,6 +39,21 @@
else:
parent.Append(helpString=help, id=id, kind=kind, item=text)
+if wx.Platform == '__WXMSW__':
+ faces = { 'times': 'Times New Roman',
+ 'mono' : 'Courier New',
+ 'helv' : 'Arial',
+ 'other': 'Comic Sans MS',
+ 'size' : 10,
+ }
+else:
+ faces = { 'times': 'Times',
+ 'mono' : 'Courier',
+ 'helv' : 'Helvetica',
+ 'other': 'new century schoolbook',
+ 'size' : 12,
+ }
+
#-------------------------------------------------------------------------------
# Graphic elements Viewer base class
#-------------------------------------------------------------------------------
@@ -300,13 +315,12 @@
self.SetDropTarget(ViewerDropTarget(self))
dc = wx.ClientDC(self)
- fontsize = 10
- self.Font = wx.Font(fontsize, wx.SWISS, wx.NORMAL, wx.NORMAL)
+ self.Font = wx.Font(faces["size"], wx.DEFAULT, wx.NORMAL, wx.NORMAL, faceName = faces["mono"])
dc.SetFont(self.Font)
width, height = dc.GetTextExtent("A")
while height > 17:
- fontsize -= 1
- self.Font = wx.Font(fontsize, wx.SWISS, wx.NORMAL, wx.NORMAL)
+ faces["size"] -= 1
+ self.Font = wx.Font(faces["size"], wx.DEFAULT, wx.NORMAL, wx.NORMAL, faceName = faces["mono"])
dc.SetFont(self.Font)
width, height = dc.GetTextExtent("A")