Add node labels and tweak node colors
This commit is contained in:
@@ -140,17 +140,26 @@ graph-editor {
|
||||
cursor: pointer;
|
||||
}
|
||||
.node.active {
|
||||
fill: #a31dfd;
|
||||
}
|
||||
.node.accepting.active {
|
||||
fill: green;
|
||||
}
|
||||
.start-arrow {
|
||||
fill: #007aff;
|
||||
stroke: none;
|
||||
}
|
||||
.start-arrow.active {
|
||||
fill: #a31dfd;
|
||||
}
|
||||
.node.accepting {
|
||||
outline: 5px solid #007aff;
|
||||
outline-offset: 4px;
|
||||
border-radius: 50%;
|
||||
}
|
||||
.node.accepting.active {
|
||||
outline: 5px solid green;
|
||||
}
|
||||
|
||||
.clickbox {
|
||||
stroke: rgba(0, 0, 0, 0);
|
||||
|
Reference in New Issue
Block a user