Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[UI] [enhancement] raw token names in alternative tactic editor display are surprising #99

Closed
rbohrer opened this issue Jan 13, 2022 · 0 comments

Comments

@rbohrer
Copy link
Member

rbohrer commented Jan 13, 2022

Version 4.9.8

Reproduce:

  1. Run the attached archive and its tactic
  2. Open the prof
  3. In the tactic editor, turn off the little circle button right next to the word "Tactic"

What I got:

  1. the commas in the tactic editor are displayed as the internal token name COMMA$ rather than a comma.
  2. UI doesn't really explain what this feature/button does anyway

Expected:

  1. If there's an easy way to document this feature, that's nice
  2. If it's some weird debugging thing and that's why it shows the token name, then it's honestly maybe fine

Priority: lowest. I'll be shocked if any student ever even uses this feature
tactic-display-on-limited-editing-redo.kyx.txt

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant