public class LemmataHandler extends java.lang.Object implements TacletSoundnessPOLoader.TacletFilter
Modifier and Type | Class and Description |
---|---|
private class |
LemmataHandler.Listener |
Modifier and Type | Field and Description |
---|---|
private LemmataAutoModeOptions |
options |
private Profile |
profile |
Constructor and Description |
---|
LemmataHandler(LemmataAutoModeOptions options,
Profile profile) |
Modifier and Type | Method and Description |
---|---|
private java.util.Collection<java.io.File> |
createFilesForAxioms(java.util.Collection<java.lang.String> filenames) |
ImmutableSet<Taclet> |
filter(java.util.List<TacletSoundnessPOLoader.TacletInfo> taclets) |
private void |
handleException(java.lang.Throwable exception) |
void |
print(java.lang.String s) |
void |
printException(java.lang.Throwable t) |
void |
println(java.lang.String s) |
private void |
saveProof(Proof p) |
void |
start() |
private void |
startProof(Proof proof) |
private void |
startProofs(ProofAggregate pa) |
private final LemmataAutoModeOptions options
private final Profile profile
public LemmataHandler(LemmataAutoModeOptions options, Profile profile)
public void println(java.lang.String s)
public void print(java.lang.String s)
public void printException(java.lang.Throwable t)
public void start() throws java.io.IOException, ProofInputException
java.io.IOException
ProofInputException
private java.util.Collection<java.io.File> createFilesForAxioms(java.util.Collection<java.lang.String> filenames)
private void handleException(java.lang.Throwable exception)
private void startProofs(ProofAggregate pa)
private void saveProof(Proof p) throws java.io.IOException
java.io.IOException
private void startProof(Proof proof)
public ImmutableSet<Taclet> filter(java.util.List<TacletSoundnessPOLoader.TacletInfo> taclets)
filter
in interface TacletSoundnessPOLoader.TacletFilter