Improved UX for editing labels in GUI - #966

Merged

tturocy merged 20 commits into

Jul 10, 2026

Commits on Jun 29, 2026

Set up label editing UX, apply to action/infoset label editing.
tturocy
committed

Commits on Jul 1, 2026

Commits on Jul 9, 2026

Commits on Jul 10, 2026

Merge branch 'master' into issue_945
tturocy
committed
Improve UX of outcome editor popup, especially with respect to duplicate/invalid label explanation
tturocy
committed