scale graphviz svg down to 2/3 of original size

This patch modifies the width and height parameters of the graphviz generated
svg image in order. This avoids having to scale the image via the browser
which may affect other tabs as well. Sadly it does not seem possible to
instruct the dot executable to generate an image at the desired scale directly.

nutils/_graph.py

@@ -71,6 +71,8 @@ def export_graphviz(self, *, fill_color: Optional[GraphvizColorCallback] = None,
                 treelog.warning('graphviz failed for error code', status.returncode)
             graph = status.stdout
             if image_type == 'svg':
+                graph = re.sub(b'(width|height)="(\d+)pt"', lambda match:
+                    b'%s="%dpt"' % (match.group(1), (int(match.group(2))*2)//3), graph, count=2)
                 i = graph.rindex(b'</svg>')
                 graph = graph[:i] + clickHandler + graph[i:]
             img.write(graph)