diff options
author | Carl Friedrich Bolz-Tereick <cfbolz@gmx.de> | 2021-02-13 12:16:34 +0100 |
---|---|---|
committer | Carl Friedrich Bolz-Tereick <cfbolz@gmx.de> | 2021-02-13 12:16:34 +0100 |
commit | f2c8950374e4aa92195b01540eb6af36153bfd38 (patch) | |
tree | bc4d72f5a76cf188d71a45caead3cacadf7e7212 /dotviewer | |
parent | updated API to cppyy_backend 1.14.2, consistent types for Win64, support for ... (diff) | |
download | pypy-f2c8950374e4aa92195b01540eb6af36153bfd38.tar.gz pypy-f2c8950374e4aa92195b01540eb6af36153bfd38.tar.bz2 pypy-f2c8950374e4aa92195b01540eb6af36153bfd38.zip |
a small hack to recognize when the screen has a lot of pixels to then allow
more zooming in and a slightly larger font size. otherwise it's not usable on
my new screen.
Diffstat (limited to 'dotviewer')
-rw-r--r-- | dotviewer/drawgraph.py | 10 | ||||
-rw-r--r-- | dotviewer/graphdisplay.py | 12 |
2 files changed, 17 insertions, 5 deletions
diff --git a/dotviewer/drawgraph.py b/dotviewer/drawgraph.py index e247c773ba..3c82391f35 100644 --- a/dotviewer/drawgraph.py +++ b/dotviewer/drawgraph.py @@ -898,11 +898,15 @@ def segmentdistance((x0,y0), (x1,y1), (x,y)): class GraphRenderer: MARGIN = 0.6 - SCALEMIN = 3 - SCALEMAX = 100 FONTCACHE = {} - def __init__(self, screen, graphlayout, scale=75): + def __init__(self, screen, graphlayout, scale=75, highdpi=False): + if highdpi: + self.SCALEMIN = 10 + self.SCALEMAX = 200 + else: + self.SCALEMIN = 3 + self.SCALEMAX = 100 self.graphlayout = graphlayout self.setscale(scale) self.setoffset(0, 0) diff --git a/dotviewer/graphdisplay.py b/dotviewer/graphdisplay.py index f07bab41dd..398e1d86aa 100644 --- a/dotviewer/graphdisplay.py +++ b/dotviewer/graphdisplay.py @@ -50,6 +50,10 @@ class Display(object): # initialize the modules by hand, to avoid initializing too much # (e.g. the sound system) pygame.display.init() + self.highdpi = pygame.display.Info().current_h > 1500 + if self.highdpi: + w *= 2 + h *= 2 pygame.font.init() self.resize((w,h)) @@ -142,7 +146,11 @@ class GraphDisplay(Display): def __init__(self, layout): super(GraphDisplay, self).__init__() - self.font = pygame.font.Font(self.STATUSBARFONT, 16) + if self.highdpi: + fontsize = 32 + else: + fontsize = 16 + self.font = pygame.font.Font(self.STATUSBARFONT, fontsize) self.viewers_history = [] self.forward_viewers_history = [] self.highlight_word = None @@ -352,7 +360,7 @@ class GraphDisplay(Display): self.viewers_history.append(self.viewer) del self.forward_viewers_history[:] self.layout = layout - self.viewer = GraphRenderer(self.screen, layout) + self.viewer = GraphRenderer(self.screen, layout, highdpi=self.highdpi) self.searchpos = 0 self.searchresults = [] self.zoom_to_fit() |