fix: fixed tikz export to retain aspect ratio

Author: pmbittner

src/main/java/org/variantsync/diffdetective/show/variation/DiffTreeApp.java

@@ -38,15 +38,20 @@
 import java.util.Map;
 
 public class DiffTreeApp extends App {
-    private final static double DEFAULT_NODE_RADIUS = 50;
+    public final static double TIKZ_NODE_RADIUS = 6.5;
+    public final static int TIKZ_FONT_SIZE = 5;
+    public final static double DEFAULT_NODE_RADIUS = 50;
+    public final static int DEFAULT_FONT_SIZE = 30;
+
     private final static Format DEFAULT_FORMAT =
             new Format(
-                    new ShowNodeFormat(),
+                    new PaperNodeFormat(),
                     // There is a bug in the exporter currently that accidentally switches direction so as a workaround we revert it here.
                     new DefaultEdgeLabelFormat(EdgeLabelFormat.Direction.ParentToChild)
             );
 
     private final static List<DiffNodeLabelFormat> AVAILABLE_FORMATS = List.of(
+            new PaperNodeFormat(),
             new ShowNodeFormat(),
             new LabelOnlyDiffNodeFormat(),
             new EditClassesDiffNodeFormat(),
@@ -175,9 +180,11 @@ private void saveTikz() {
                     var unbufferedOutput = Files.newOutputStream(targetFile.toPath());
                     var output = new BufferedOutputStream(unbufferedOutput)
             ) {
+                final double millimetersPerPixel = TIKZ_NODE_RADIUS / resolution.x();
                 final Vec2 flipY  = new Vec2(1.0, -1.0);
-                final double nodeRadiusInTikz = 6.5;
-                final Vec2 scaleToTikz = Vec2.all(nodeRadiusInTikz).dividedBy(resolution);
+                final Vec2 scaleToTikz =
+                        Vec2.all(millimetersPerPixel);
+//                        Vec2.all(TIKZ_NODE_RADIUS).dividedBy(resolution);
 
                 tikzExporter.exportDiffTree(
                         diffTree,
@@ -187,7 +194,8 @@ private void saveTikz() {
                             pos = pos.scale(scaleToTikz);
                             return pos;
                         },
-                        output
+                        output,
+                        true
                         );
             } catch (IOException e) {
                 JOptionPane.showMessageDialog(

src/main/java/org/variantsync/diffdetective/show/variation/GraphNodeGraphics.java

@@ -18,7 +18,7 @@ public class GraphNodeGraphics extends EntityGraphics {
     double textbox_borderwidth_absolute = 2;
     double textbox_insets_absolute = 12;
     int textbox_borderarcwidth_absolute = 7;
-    Font basic = new Font(null, Font.PLAIN, 20);
+    Font basic = new Font(null, Font.PLAIN, DiffTreeApp.DEFAULT_FONT_SIZE);
 
     public GraphNodeGraphics(NodeView node) {
         this.node = node;

src/main/java/org/variantsync/diffdetective/variation/diff/serialize/TikzExporter.java

@@ -16,6 +16,8 @@
 import java.util.Map;
 import java.util.function.Function;
 import java.util.stream.Collectors;
+import java.util.stream.Stream;
+
 
 /**
  * Exporter for TikZ pictures which can be embedded into a LaTeX document.
@@ -69,13 +71,15 @@ public void exportDiffTree(
         exportDiffTree(
                 diffTree,
                 positions::get,
-                destination);
+                destination,
+                true);
     }
 
     public void exportDiffTree(
             DiffTree diffTree,
             Function<DiffNode, Vec2> nodeLayout,
-            OutputStream destination
+            OutputStream destination,
+            boolean escape
     ) {
         // Start tikz picture.
         var output = new PrintStream(destination);
@@ -101,24 +105,25 @@ public void exportDiffTree(
         output.format("%n\t\\draw[vtdarrow]");
         format.forEachEdge(diffTree, (edge) -> {
             output.format("%n\t\t(node_%d) edge[%s] (node_%d)",
-                edge.from().getID(),
-                edge.style().tikzStyle(),
-                edge.to().getID());
+                    edge.from().getID(),
+                    edge.style().tikzStyle(),
+                    edge.to().getID());
         });
         output.println();
         output.format("%n\t;");
         output.println();
 
         // Draw node labels. We do this last so that they are on top of edges and nodes.
         format.forEachNode(diffTree, (node) -> {
-            String escapedLabel =
+            Stream<String> labels =
                     format
                             .getNodeFormat()
                             .toMultilineLabel(node)
-                            .stream()
-                            .map(LaTeX::escape)
-                            .collect(Collectors
-                                    .joining(" \\\\ "));
+                            .stream();
+            if (escape) {
+                labels = labels.map(LaTeX::escape);
+            }
+            String escapedLabel = labels.collect(Collectors.joining(" \\\\ "));
 
             output.format("\t\\node[textbox] at (%s) {%s};%n",
                     node.getID(),

src/main/java/org/variantsync/diffdetective/variation/diff/serialize/nodeformat/PaperNodeFormat.java

@@ -0,0 +1,54 @@
+package org.variantsync.diffdetective.variation.diff.serialize.nodeformat;
+
+import org.prop4j.NodeWriter;
+import org.variantsync.diffdetective.util.LaTeX;
+import org.variantsync.diffdetective.util.StringUtils;
+import org.variantsync.diffdetective.variation.NodeType;
+import org.variantsync.diffdetective.variation.diff.DiffNode;
+
+import java.util.Arrays;
+import java.util.List;
+
+public class PaperNodeFormat implements DiffNodeLabelFormat {
+    public static final int MAX_ARTIFACT_LABEL_LENGTH = 12;
+
+    @Override
+    public String toLabel(DiffNode node) {
+        if (node.isRoot()) {
+            return "r";
+        }
+
+        String s = "";
+
+        if (node.isAnnotation()) {
+//            if (node.getNodeType() == NodeType.ELSE) {
+//                s += "ELSE";
+//            } else {
+              s += node.getFormula().toString(NodeWriter.logicalSymbols);
+//            }
+        } else {
+            final int lineNoFrom = node.getFromLine().inDiff();
+            final int lineNoTo   = node.getToLine().inDiff();
+            s += lineNoFrom;
+            if (lineNoFrom != lineNoTo - 1) {
+                s += "-" + lineNoTo;
+            }
+
+            s += ": ";
+
+
+            String label = node.getLabel().toString().trim();
+            if (label.length() > MAX_ARTIFACT_LABEL_LENGTH) {
+                label = StringUtils.clamp(MAX_ARTIFACT_LABEL_LENGTH - 3, label) + "...";
+            }
+            s += label; //LaTeX.escape(label);
+        }
+
+        return s;
+    }
+
+    @Override
+    public List<String> toMultilineLabel(DiffNode node) {
+        return Arrays.stream(toLabel(node).split(StringUtils.LINEBREAK)).toList();
+    }
+}