From 712adb53f96583a4bbfb911ce5672ce1c80d041c Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Tue, 7 Nov 2023 14:03:58 +0100
Subject: [PATCH] Put variant on same line as keyword when pretty-printing
---
.../org/eventb/texttools/prettyprint/MachinePrintSwitch.java | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/org.eventb.texttools/src/org/eventb/texttools/prettyprint/MachinePrintSwitch.java b/org.eventb.texttools/src/org/eventb/texttools/prettyprint/MachinePrintSwitch.java
index bf54a60..ff6b274 100644
--- a/org.eventb.texttools/src/org/eventb/texttools/prettyprint/MachinePrintSwitch.java
+++ b/org.eventb.texttools/src/org/eventb/texttools/prettyprint/MachinePrintSwitch.java
@@ -251,7 +251,7 @@ public class MachinePrintSwitch extends MachineSwitch<Boolean> implements
printer.appendLineBreak();
}
- printer.appendWithLineBreak(VARIANT);
+ printer.appendWithSpace(VARIANT);
printer.increaseIndentLevel();
for (final Variant variant : variants) {
--
GitLab