|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Object fmrisc.ProofNavigator.State
public final class State
Execution context for the proof navigator.
Field Summary | |
---|---|
static java.lang.String |
NamespacePrefix
|
static java.lang.String |
NamespaceURI
|
static java.lang.String |
OMDocPrefix
|
static java.lang.String |
OMDocURI
|
static java.lang.String |
OpenMathPrefix
|
static java.lang.String |
OpenMathURI
|
static java.lang.String |
XMLPrefix
|
static java.lang.String |
XMLURI
|
Constructor Summary | |
---|---|
State()
|
Method Summary | |
---|---|
static Context |
getContext()
get context used by proof navigator |
static Environment |
getEnvironment()
get environment used by proof navigator |
static java.lang.String |
getError()
get error message set |
static java.util.Stack |
getFileStack()
Get file stack. |
static CVCLFormulaMask |
getFormulaMask()
Get formula mask. |
static Environment |
getGlobal()
get global environment of proof navigator |
static boolean |
getLabels()
ask whether lexer shall produce labels rather than idents |
static Expression |
getLastTCC()
get last type checking condition |
static PNLexer |
getLexer()
get lexer used by proof navigator |
static Presenter |
getPresenter()
Get current presenter. |
static Proof |
getProof()
get current proof |
static Prover |
getProver()
get prover currently in use |
static java.io.PrintWriter |
getProverLog()
Get prover log |
static java.util.Stack |
getReaderStack()
Get reader stack. |
static ProofState[] |
getReplayChildren()
Set children of current proof state during proof replay. |
static Prover |
getRunningProver()
Get prover currently running. |
static int |
getServerPort()
Get server port. |
static Store |
getStore()
Get current store. |
static java.io.BufferedReader |
getSystemIn()
get standard input stream |
static java.io.PrintWriter |
getSystemOut()
get standard output stream |
static boolean |
init(java.lang.String name,
java.lang.String cvcl)
Initialize prover state using denoted context. |
static boolean |
isAborted()
Get prover abort state. |
static Prover |
newProver(java.io.PrintWriter log,
int timeout,
boolean mask)
get new instance of a prover |
static void |
resetError()
reset error message |
static void |
setAborted(boolean aborted)
Set prover abort state. |
static void |
setAutoSimplify(boolean on)
Turn on/off automatic simplification |
static void |
setBigFont(boolean big)
Set font size. |
static void |
setEnvironment(Environment env)
set environment used by proof navigator |
static void |
setError(java.lang.String error)
set error message, does not override previously set message |
static void |
setFormulaMask(CVCLFormulaMask mask)
Set formula mask. |
static void |
setLabels(boolean signal)
signal that lexer shall produce labels rather than idents |
static void |
setLastTCC(Expression tcc)
set last type checking condition |
static void |
setLexer(PNLexer lexer)
set lexer used by proof navigator |
static void |
setProof(Proof proof)
set current proof |
static void |
setReplayChildren(ProofState[] children)
Set children of current proof state during proof replay. |
static void |
setRunningProver(Prover prover)
Set prover currently running. |
static void |
setServerPort(int port)
Set server port. |
static void |
setSystemIn(java.io.BufferedReader in)
set standard input stream |
static void |
setSystemOut(java.io.PrintWriter out)
set standard output stream |
static void |
skipNL()
Skip new line from input stream |
static boolean |
useAutoSimplify()
Is automatic simplification used? |
static boolean |
useBigFont()
Get font size. |
Methods inherited from class java.lang.Object |
---|
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Field Detail |
---|
public static final java.lang.String NamespacePrefix
public static final java.lang.String NamespaceURI
public static final java.lang.String OpenMathPrefix
public static final java.lang.String OpenMathURI
public static final java.lang.String OMDocPrefix
public static final java.lang.String OMDocURI
public static final java.lang.String XMLPrefix
public static final java.lang.String XMLURI
Constructor Detail |
---|
public State()
Method Detail |
---|
public static boolean init(java.lang.String name, java.lang.String cvcl)
name
- the name (path) of the context (if null, default name is used)cvcl
- the name (path) to the "cvcl" executable
public static Prover newProver(java.io.PrintWriter log, int timeout, boolean mask)
log
- stream for prover to write log messages to (null, if none)timeout
- timeout for prover in seconds (0, if none)mask
- true iff quantified formulas are to be masked
public static java.io.PrintWriter getSystemOut()
public static void setSystemOut(java.io.PrintWriter out)
out
- standard output stream used by systempublic static java.io.BufferedReader getSystemIn()
public static void setSystemIn(java.io.BufferedReader in)
in
- standard input stream used by systempublic static void skipNL()
public static void setLastTCC(Expression tcc)
tcc
- the type checking condition generated lastpublic static Expression getLastTCC()
public static void setLexer(PNLexer lexer)
lexer
- used by the proof navigatorpublic static PNLexer getLexer()
public static void setLabels(boolean signal)
signal
- true iff lexer shall produce labelspublic static boolean getLabels()
public static void setError(java.lang.String error)
error
- the error messagepublic static void resetError()
public static java.lang.String getError()
public static void setEnvironment(Environment env)
env
- environment to be used by proof navigatorpublic static Environment getEnvironment()
public static Environment getGlobal()
public static Context getContext()
public static Prover getProver()
public static void setRunningProver(Prover prover)
prover
- currently running prover.public static Prover getRunningProver()
public static void setProof(Proof proof)
proof
- proof currently under development (null, if none)public static Proof getProof()
public static Store getStore()
public static Presenter getPresenter()
public static java.io.PrintWriter getProverLog()
public static java.util.Stack getFileStack()
public static java.util.Stack getReaderStack()
public static CVCLFormulaMask getFormulaMask()
public static void setFormulaMask(CVCLFormulaMask mask)
mask
- the formula mask.public static void setServerPort(int port)
port
- the port used by the command serverpublic static int getServerPort()
public static void setAborted(boolean aborted)
aborted
- true if the prover has been aborted.public static boolean isAborted()
public static void setBigFont(boolean big)
big
- true iff big fonts are to be displayed.public static boolean useBigFont()
public static void setReplayChildren(ProofState[] children)
children
- the children states (null, if none).public static ProofState[] getReplayChildren()
public static void setAutoSimplify(boolean on)
on
- true iff automatic simplification is turned on.public static boolean useAutoSimplify()
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |