fixes a bug in the fsm svg export

This commit is contained in:
hneemann 2020-05-28 19:45:42 +02:00
parent 1544c26faf
commit 712d7fcdd7

View File

@ -167,9 +167,9 @@ public class Transition extends Movable<Transition> {
// text // text
ArrayList<String> strings = new ArrayList<>(); ArrayList<String> strings = new ArrayList<>();
if (condition != null && !condition.isEmpty()) if (condition != null && !condition.isEmpty())
strings.add(condition); strings.add("$" + condition + "$");
if (getValues() != null && !getValues().isEmpty()) if (getValues() != null && !getValues().isEmpty())
strings.add(Lang.get("fsm_set_N", getValues())); strings.add(Lang.get("fsm_set_N", "$" + getValues() + "$"));
if (!strings.isEmpty()) { if (!strings.isEmpty()) {
final int fontSize = Style.NORMAL.getFontSize(); final int fontSize = Style.NORMAL.getFontSize();
@ -186,7 +186,7 @@ public class Transition extends Movable<Transition> {
} }
for (String s : strings) { for (String s : strings) {
gr.drawText(textPos, s, Orientation.CENTERCENTER, Style.INOUT); gr.drawText(textPos, s, Orientation.CENTERCENTER, Style.NORMAL);
textPos = textPos.add(0, fontSize); textPos = textPos.add(0, fontSize);
} }
} }