de.uka.ilkd.key.proof.io

Interface IProofFileParser

All Known Implementing Classes:

IntermediatePresentationProofFileParser

public interface IProofFileParser

Defines the required which a KeYParser needs to parse a *.proof file and to apply the rules again.

Author:

Martin Hentschel

Nested Class Summary

Nested Classes

Modifier and Type	Interface and Description
static class	IProofFileParser.ProofElementID Enumeration of the different syntactic elements occurring in a saved proof tree representation.

Method Summary

Modifier and Type	Method and Description
void	beginExpr(IProofFileParser.ProofElementID eid, java.lang.String str)
void	endExpr(IProofFileParser.ProofElementID eid, int stringLiteralLine)
java.util.List<java.lang.Throwable>	getErrors()
java.lang.String	getStatus()

Method Detail

beginExpr

void beginExpr(IProofFileParser.ProofElementID eid,
               java.lang.String str)

endExpr

void endExpr(IProofFileParser.ProofElementID eid,
             int stringLiteralLine)

getStatus

java.lang.String getStatus()

getErrors

java.util.List<java.lang.Throwable> getErrors()