From 448f9122c87cbb92ba33fa6ccb07b9ddb3b1638a Mon Sep 17 00:00:00 2001
From: Jette Petzold <jep@informatik.uni-kiel.de>
Date: Wed, 8 May 2024 15:39:41 +0200
Subject: [PATCH] scaling for snippets

---
 extension/src-webview/snippets/snippet-renderer.tsx | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/extension/src-webview/snippets/snippet-renderer.tsx b/extension/src-webview/snippets/snippet-renderer.tsx
index c84346f..81bf72c 100644
--- a/extension/src-webview/snippets/snippet-renderer.tsx
+++ b/extension/src-webview/snippets/snippet-renderer.tsx
@@ -31,6 +31,8 @@ export class SnippetRenderer {
     protected modelRenderer: ModelRenderer;
     /** Needed to show labels and edges. */
     protected bounds: Bounds;
+    /** Scale factor for the snippet graphs. */
+    protected scale = 0.8;
 
     setModelRenderer(renderer: ModelRenderer): void {
         this.modelRenderer = renderer;
@@ -58,10 +60,15 @@ export class SnippetRenderer {
             const width = ((snippet.graph as SGraph).children[0] as SNode).size.width + 30;
             const height = ((snippet.graph as SGraph).children[0] as SNode).size.height + 30;
             if (graph?.data?.attrs) {
-                graph.data.attrs["width"] = width;
-                graph.data.attrs["height"] = height;
+                graph.data.attrs["width"] = width * this.scale;
+                graph.data.attrs["height"] = height * this.scale;
                 graph.data.attrs["id"] = snippet.id;
             }
+            // scale the graph to fit the sidebar better
+            if (graph?.children && (graph.children[0] as VNode).data?.attrs) {
+                (graph.children[0] as VNode).data!.attrs!["transform"] = `scale(${this.scale}) translate(0,0)`;
+            }
+
             const result: VNode = <div>{graph}</div>;
             return result;
         });