[parser/printer?] KeYmaera X allows uploading models with Unicode characters, then errs

[rbohrer]

Version: 4.9.8 OS: Windows 10

Reproduce:

• Upload attached archive
• Start Proof -> run Auto

Got:

• Says proof successful, but then UI hangs during the final "checking proof" step. Opening the web dev console reveals that KeYmaera X saved a lemma to lemmadb, read it back, and got a lemma that didn't match. In the non-matching version, the "problem" section looks like this: ? x x - x + x = x

Expected:

• Either give an error message upon upload for Unicode characters, or treat them identically to the non-Unicode keywords

Priority: This is my first bug report that comes from one of my students. Although it's easy to teach around, I actually would expect both CMU and WPI students to run into this issue in future semesters. See also added commentary

Added commentary: In my own work, I usually don't run into this problem by uploading a whole new model (like the student did). Usually I run into a problem where I copy-paste Unicode from the UI and it looks like ASCII so I forget it's not. In particular, the Unicode minus symbol looks very similar to the standard ASCII hyphen-minus, but leads to similar errors. So it's quite easy to get confused upon copy-pasting a minus.

UnicodeSurprise.kyx.txt

[smitsch]

Fixed in f6ca63bf9a6804a3ed22ed776190880ecfb074f2