displayname of Taclets need to be free of spaces.

[wadoon]

Description

A proof can not be reloaded by KeY if a Taclet was used which (a) contains spaces in the \displayname meta-information and (b) has user-defined variable.

In the background, KeY writes a term definition in the proof file containing an origin clause using the \displayname. This term definition, especially, the origin label definition is wrong and leads to an exception.

Reproducible

Is the issue reproducible?

always

Steps to reproduce

Describe the steps needed to reproduce the issue.

1. Define a (or modify) taclet to have a \displayname with spaces.

   test_assume { \schemavar formula phi; \add(phi ==>); \displayname "Test Test" }; 
   

2. Use the taclet in a proof.
3. Store and reload the proof.
4. Observe an exception like this:

(Well-formed origins have one of the following formats: "spec_type @ file <file name> @ line <line number>")
spec_type @ node <node number> (<rule name>)")
spec_type (implicit)")

• Commit: be8c6af