Use KeYParser.g4 for parsing proof scripts #3021

This MR get rid of the hand-written parser for proof scripts and uses a few rules in KeYParser.g4 instead.

Since the start of proof scripts, the KeYParser has changed and became an ANTLR4 grammar. This allows us to easily write grammar for our proof scripts. (Or just copy the few rules from Sarah and mine proof script parser). This eliminates the handwritten proof script parser with the following benefits:

1. Proof Scripts are a first-class citizen in KeY files. You do not need to put your proof script into a string literal: \proofscript { andLeft; andRight; rule a ==> b; }

Please note an ambiguity in the grammar: rule b ==> c could either be interpreted as a command with one or two arguments: 1. a semi-sequent b ==> and a term c, or 2. a sequent b ==> c.

Use quotes or better backticks to clarify these situations.

1. Earlier and better syntax errors. (during reading the KeY file)

2. Proper data structure: no triple of strings are pushed through KeY.

3. You do not need to put your arguments in quotes. Literals, terms and sequents are parsed.

Tried to achieve backwards-compatibility. If the proof script is given as a string, the parsing is delayed until the execution. The same is valid for arguments.

Note there is a difference between f(x) and "f(x)". The first one is parsed directly as a term and cannot be passed to non-term arguments. The second one is parsed as a string. By meta-information on commands, the string is lazily converted to a term if necessary.