public class OutputStreamProofSaver extends Object
OutputStream
.Modifier and Type | Field and Description |
---|---|
protected String |
internalVersion |
(package private) LogicPrinter |
printer |
protected Proof |
proof |
Constructor and Description |
---|
OutputStreamProofSaver(Proof proof) |
OutputStreamProofSaver(Proof proof,
String internalVersion) |
Modifier and Type | Method and Description |
---|---|
String |
builtinRuleIfInsts(Node node,
ImmutableList<PosInOccurrence> ifInsts) |
private StringBuffer |
collectProof(Node node,
String prefix,
StringBuffer tree) |
private static LogicPrinter |
createLogicPrinter(Services serv,
boolean shortAttrNotation) |
static String |
escapeCharacters(String toEscape)
double escapes quotation marks and backslashes to be storeable in a text file
|
protected String |
getBasePath() |
String |
getInteresting(SVInstantiations inst) |
String |
ifFormulaInsts(Node node,
ImmutableList<IfFormulaInstantiation> l) |
private String |
makePathsRelative(String header)
Searches in the header for absolute paths to Java files and tries to replace them
by paths relative to the proof file to be saved.
|
private String |
newNames2Proof(Node n) |
String |
node2Proof(Node node) |
static String |
posInOccurrence2Proof(Sequent seq,
PosInOccurrence pos) |
static String |
posInTerm2Proof(PosInTerm pos) |
static String |
printAnything(Object val,
Services services) |
static StringBuffer |
printAnything(Object val,
Services services,
boolean shortAttrNotation) |
static StringBuffer |
printProgramElement(ProgramElement pe) |
private static StringBuffer |
printSequent(Sequent val,
Services services) |
private void |
printSingleNode(Node node,
String prefix,
StringBuffer tree) |
static StringBuffer |
printTerm(Term t,
Services serv) |
static StringBuffer |
printTerm(Term t,
Services serv,
boolean shortAttrNotation) |
void |
save(OutputStream out) |
private static String |
tryToMakeFilenameRelative(String absPath,
String basePath)
Try to create a relative path, but return the absolute path
if a relative path cannot be found.
|
private void |
userInteraction2Proof(Node node,
StringBuffer tree) |
StringBuffer |
writeLog(Proof p) |
String |
writeProfile(Profile profile) |
String |
writeSettings(ProofSettings ps) |
protected final Proof proof
protected final String internalVersion
LogicPrinter printer
public OutputStreamProofSaver(Proof proof)
public StringBuffer writeLog(Proof p)
public String writeSettings(ProofSettings ps)
public void save(OutputStream out) throws IOException
IOException
protected String getBasePath() throws IOException
IOException
private String makePathsRelative(String header)
private static String tryToMakeFilenameRelative(String absPath, String basePath)
private void printSingleNode(Node node, String prefix, StringBuffer tree)
private StringBuffer collectProof(Node node, String prefix, StringBuffer tree)
private void userInteraction2Proof(Node node, StringBuffer tree)
public static String posInOccurrence2Proof(Sequent seq, PosInOccurrence pos)
public String getInteresting(SVInstantiations inst)
public String ifFormulaInsts(Node node, ImmutableList<IfFormulaInstantiation> l)
public String builtinRuleIfInsts(Node node, ImmutableList<PosInOccurrence> ifInsts)
public static String escapeCharacters(String toEscape)
toEscape
- the String to double escapepublic static StringBuffer printProgramElement(ProgramElement pe)
public static StringBuffer printTerm(Term t, Services serv)
public static StringBuffer printTerm(Term t, Services serv, boolean shortAttrNotation)
public static StringBuffer printAnything(Object val, Services services, boolean shortAttrNotation)
private static StringBuffer printSequent(Sequent val, Services services)
private static LogicPrinter createLogicPrinter(Services serv, boolean shortAttrNotation)