de.uka.ilkd.key.proof.io

Class ProofSaver

java.lang.Object

de.uka.ilkd.key.proof.io.OutputStreamProofSaver

de.uka.ilkd.key.proof.io.ProofSaver

Direct Known Subclasses:

GZipProofSaver

public class ProofSaver
extends OutputStreamProofSaver

Saves a proof and provides useful methods for pretty printing terms or programs.

Field Summary

Fields

Modifier and Type	Field and Description
private java.io.File	file
private static java.util.List<ProofSaverListener>	listeners Contains all listener.

Fields inherited from class de.uka.ilkd.key.proof.io.OutputStreamProofSaver

internalVersion, printer, proof

Constructor Summary

Constructors

Constructor and Description
ProofSaver(Proof proof, java.io.File file)
ProofSaver(Proof proof, java.io.File file, java.lang.String internalVersion)
ProofSaver(Proof proof, java.lang.String fileName, java.lang.String internalVersion)

Method Summary

Modifier and Type	Method and Description
static void	addProofSaverListener(ProofSaverListener l) Adds the ProofSaverListener.
static java.lang.String	computeBasePath(java.io.File proofFile) Computes the base path of the given proof File.
private java.lang.String	filename()
protected static void	fireProofSaved(ProofSaverEvent e) Informs all listener about the event ProofSaverListener.proofSaved(ProofSaverEvent).
protected java.lang.String	getBasePath()
static void	removeProofSaverListener(ProofSaverListener l) Removes the ProofSaverListener.
java.lang.String	save()
protected void	save(java.io.File file) Save the proof to file referenced by file.

Methods inherited from class de.uka.ilkd.key.proof.io.OutputStreamProofSaver

builtinRuleIfInsts, escapeCharacters, getInteresting, getJavaSourceLocation, ifFormulaInsts, node2Proof, posInOccurrence2Proof, posInTerm2Proof, printAnything, printAnything, printProgramElement, printTerm, printTerm, save, writeLog, writeProfile, writeSettings

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

file

private final java.io.File file

listeners

private static final java.util.List<ProofSaverListener> listeners

Contains all listener.

They are used for instance by the Eclipse integration to refresh the workspace when a proof file was saved.

.

Constructor Detail

ProofSaver

public ProofSaver(Proof proof,
                  java.lang.String fileName,
                  java.lang.String internalVersion)

ProofSaver

public ProofSaver(Proof proof,
                  java.io.File file)

ProofSaver

public ProofSaver(Proof proof,
                  java.io.File file,
                  java.lang.String internalVersion)

Method Detail

save

protected void save(java.io.File file)
             throws java.io.IOException

Save the proof to file referenced by file. The format in which the proof is stored depends on the class. Thr base class creates a plain output file. Subclasses may choose to use other formats.

Parameters:

file - the file to write to

Throws:

java.io.IOException - if I/O fails

save

public java.lang.String save()
                      throws java.io.IOException

Throws:

java.io.IOException

getBasePath

protected java.lang.String getBasePath()
                                throws java.io.IOException

Overrides:

getBasePath in class OutputStreamProofSaver

Throws:

java.io.IOException

computeBasePath

public static java.lang.String computeBasePath(java.io.File proofFile)
                                        throws java.io.IOException

Computes the base path of the given proof File.

This method is used by getBasePath() and by the Eclipse integration.

Parameters:

proofFile - The proof File.

Returns:

The computed base path of the given proof File.

Throws:

java.io.IOException - Occurred Exception.

addProofSaverListener

public static void addProofSaverListener(ProofSaverListener l)

Adds the ProofSaverListener.

Parameters:

l - The ProofSaverListener to add.

removeProofSaverListener

public static void removeProofSaverListener(ProofSaverListener l)

Removes the ProofSaverListener.

Parameters:

l - The ProofSaverListener to remove.

fireProofSaved

protected static void fireProofSaved(ProofSaverEvent e)

Informs all listener about the event ProofSaverListener.proofSaved(ProofSaverEvent).

Parameters:

e - The event.

filename

private java.lang.String filename()