LS-Lab/KeYmaeraX-release

[UI] [enhancement] Not obvious to user why diRule breaks tactic editor goal-switching

rbohrer opened this issue · 6 comments

rbohrer commented

Version: 4.9.8
Reproduce:

  1. run attached archive's tactic
  2. open proof interface
  3. go to tactic editor
  4. try to navigate to the second TODO under "dC". It won't let you and the user won't know why

I'm assuming it's by-design that you can't navigate to these "todos" and that it's a result of the expandAllDefs and delayed USubst. However it may look like a bug to users without any added context.

Low priority, easy to explain to students

tactic-display-on-limited-editing-redo.kyx.txt

smitsch commented

The attached archive seems to not fit the bug description, please update.

rbohrer commented

Updated file and description, my bad! I believe the same applies to issue #99, will check that now too

smitsch commented

Was unable to reproduce it, may have been fixed with some earlier improvement. Please check.

rbohrer commented

I built the latest commit (6211d34) and reproduced the bug. To clarify: when I click on the second TODO, the mouse cursor will move, but the arrow symbol and green bar do not move, and the UI does not navigate to the second tab.

Additional info:
OS: Windows 10 Enterprise
Browser: Chrome Version 97.0.4692.71 (Official Build) (64-bit)
JDK: Openjdk 11.0.13

Let me know if you need anything else, thanks!

smitsch commented

Still not able to reproduce. Is there anything useful in the View->Developer->JavaScript Console in Chrome?

rbohrer commented