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 to scale it down to 2/3 the original size. 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. The regular expression that is used
instead is fairly sensitive to the generated xml, but that is acceptable given
that the only risk is to leave the svg at its original scale.

nutils/_graph.py

@@ -5,6 +5,7 @@
 import subprocess
 import abc
 import html
+import re
 
 Metadata = TypeVar('Metadata')
 GraphvizColorCallback = Callable[['Node'], Optional[str]]
@@ -70,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'<svg width="(\d+)pt" height="(\d+)pt"', lambda match:
+                    b'<svg width="%dpt" height="%dpt"' % tuple((int(l)*2)//3 for l in match.groups()), graph, count=1)
                 i = graph.rindex(b'</svg>')
                 graph = graph[:i] + clickHandler + graph[i:]
             img.write(graph)