mirror of
https://github.com/hneemann/Digital.git
synced 2025-09-16 16:34:47 -04:00
minor improvement of fsm layout
This commit is contained in:
parent
5ec2bf496f
commit
c41dc3a387
@ -82,7 +82,7 @@ public class Transition extends Movable<Transition> {
|
|||||||
|
|
||||||
for (Transition t : transitions)
|
for (Transition t : transitions)
|
||||||
if (t != this)
|
if (t != this)
|
||||||
addRepulsive(t.getPos(), 800);
|
addRepulsive(t.getPos(), 1800);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -131,8 +131,13 @@ public class Transition extends Movable<Transition> {
|
|||||||
final VectorFloat arrowTip = toState.getPos().add(difToTip);
|
final VectorFloat arrowTip = toState.getPos().add(difToTip);
|
||||||
|
|
||||||
Polygon p = new Polygon(false)
|
Polygon p = new Polygon(false)
|
||||||
.add(start)
|
.add(start);
|
||||||
.add(anchorFrom, anchorTo, end);
|
|
||||||
|
if (anchorFrom.equals(anchorTo))
|
||||||
|
p.add(anchorFrom, end);
|
||||||
|
else
|
||||||
|
p.add(anchorFrom, anchorTo, end);
|
||||||
|
|
||||||
final Style arrowStyle = Style.SHAPE_PIN;
|
final Style arrowStyle = Style.SHAPE_PIN;
|
||||||
gr.drawPolygon(p, arrowStyle);
|
gr.drawPolygon(p, arrowStyle);
|
||||||
|
|
||||||
|
Loading…
x
Reference in New Issue
Block a user