Missing spaces in .key files are ignored

[mattulbrich]

Description

In a .key file, there needs not be a space after a \backslash_keyword. But this should be reported.

Reproducible

always

Steps to reproduce

Load the following example

\rules {
  \lemmanospaces {
  \schemaVar \termint t;
  \find(t+0)
  \replacewith(t)
  };
}

\problem { 5+0=5 }

It will parse – unexpectedly. You can then also apply the rule "nospaces".

It should not parse

Additional information

The problem is that there is no lexer rule for essentially \[a-z]* in the key lexer which would match againt "\termint" to rule it out.
Perhaps adding that lexer rule would solve the issue.

(I assign this to Alexander @wadoon since he implemented the new KeYParser.)

---

• Commit: 627d745

[wadoon]

fix on #3021

[mattulbrich]

#3021 is quite a heavyweight change touching 70 files which happens to include the onliner

which fixes this issue.

[wadoon]

I was just on this branch, fixed it there. What is needed is the line above, and some fixes in the KeY file, (e.g., b6201c6#diff-a47d36ef63c8dd7f5770c4f9c4ded9efbfc5bee601e0d8b7e645ab3f0f21d322)

Errors in the key formatter were hidden by this "feature":