public class OutputStreamProofSaver
extends java.lang.Object
OutputStream
.Modifier and Type | Field and Description |
---|---|
protected java.lang.String |
internalVersion |
protected Proof |
proof |
Constructor and Description |
---|
OutputStreamProofSaver(Proof proof) |
OutputStreamProofSaver(Proof proof,
java.lang.String internalVersion) |
Modifier and Type | Method and Description |
---|---|
java.lang.String |
builtinRuleIfInsts(Node node,
ImmutableList<PosInOccurrence> ifInsts) |
static java.lang.String |
escapeCharacters(java.lang.String toEscape)
double escapes quotation marks and backslashes to be storeable in a text
file
|
protected java.lang.String |
getBasePath() |
java.lang.String |
getInteresting(SVInstantiations inst) |
static java.io.File |
getJavaSourceLocation(Proof proof)
Extracts java source directory from
Proof.header() , if it exists. |
java.lang.String |
ifFormulaInsts(Node node,
ImmutableList<IfFormulaInstantiation> l) |
void |
node2Proof(Node node,
java.lang.Appendable ps)
Print applied rule(s) for a proof node and its decendants into the passed writer
such that in can be loaded again as a proof.
|
static java.lang.String |
posInOccurrence2Proof(Sequent seq,
PosInOccurrence pos) |
static java.lang.String |
posInTerm2Proof(PosInTerm pos) |
static java.lang.String |
printAnything(java.lang.Object val,
Services services) |
static java.lang.StringBuffer |
printAnything(java.lang.Object val,
Services services,
boolean shortAttrNotation) |
static java.lang.StringBuffer |
printProgramElement(ProgramElement pe) |
static java.lang.StringBuffer |
printTerm(Term t,
Services serv) |
static java.lang.StringBuffer |
printTerm(Term t,
Services serv,
boolean shortAttrNotation) |
void |
save(java.io.OutputStream out) |
java.lang.StringBuffer |
writeLog()
Write users and KeY versions to buffer.
|
java.lang.String |
writeProfile(Profile profile) |
java.lang.String |
writeSettings(ProofSettings ps) |
protected final Proof proof
protected final java.lang.String internalVersion
public OutputStreamProofSaver(Proof proof)
public OutputStreamProofSaver(Proof proof, java.lang.String internalVersion)
public static java.io.File getJavaSourceLocation(Proof proof)
Proof.header()
, if it exists.proof
- the Proofpublic java.lang.StringBuffer writeLog()
public java.lang.String writeProfile(Profile profile)
public java.lang.String writeSettings(ProofSettings ps)
public void save(java.io.OutputStream out) throws java.io.IOException
java.io.IOException
protected java.lang.String getBasePath() throws java.io.IOException
java.io.IOException
public void node2Proof(Node node, java.lang.Appendable ps) throws java.io.IOException
node
- the proof node from which to be printedps
- the writer in which the rule(s) is/are printedjava.io.IOException
- an exception thrown when printing failspublic static java.lang.String posInOccurrence2Proof(Sequent seq, PosInOccurrence pos)
public static java.lang.String posInTerm2Proof(PosInTerm pos)
public java.lang.String getInteresting(SVInstantiations inst)
public java.lang.String ifFormulaInsts(Node node, ImmutableList<IfFormulaInstantiation> l)
public java.lang.String builtinRuleIfInsts(Node node, ImmutableList<PosInOccurrence> ifInsts)
public static java.lang.String escapeCharacters(java.lang.String toEscape)
toEscape
- the String to double escapepublic static java.lang.StringBuffer printProgramElement(ProgramElement pe)
public static java.lang.StringBuffer printTerm(Term t, Services serv, boolean shortAttrNotation)
public static java.lang.String printAnything(java.lang.Object val, Services services)
public static java.lang.StringBuffer printAnything(java.lang.Object val, Services services, boolean shortAttrNotation)
Copyright © 2003-2019 The KeY-Project.