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

[rbohrer]

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]

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

[rbohrer]

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

[smitsch]

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

[rbohrer]

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]

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

[rbohrer]

I don't think so from last time I checked but it may be after the next release when I get chance to debug again in depth so feel free to let it wait until after release

…

On Thu, Feb 3, 2022, 4:57 PM Stefan Mitsch ***@***.***> wrote: Still not able to reproduce. Is there anything useful in the View->Developer->JavaScript Console in Chrome? — Reply to this email directly, view it on GitHub <#98 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAO6WYKV2OYP7MG5JLIRDJDUZL24PANCNFSM5L4C6JJQ> . Triage notifications on the go with GitHub Mobile for iOS <https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> or Android <https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>. You are receiving this because you authored the thread.Message ID: ***@***.***>