fmrisc.ProofNavigator.Communication

Class Presenter

java.lang.Object

fmrisc.ProofNavigator.Communication.Presenter

public final class Presenter
extends java.lang.Object

Interface to visual presentation of declarations and proof states.

Constructor Summary

Constructors

Constructor and Description
Presenter(java.io.File directory) Create instance of presenter with files in denoted directory.

Method Summary

Modifier and Type	Method and Description
java.io.File	getDeclFile() Get file where all declarations are stored
java.io.File	getFile(ProofState state) Construct file name for proof state
org.w3c.dom.Element	getRoot(org.w3c.dom.Document document) Get root node of document to which new nodes should be appended.
boolean	newDeclarations() Creates new declaration document.
void	resize() Update font size depending on user settings.
boolean	updateDeclarations() Update the declarations written so far (rewriting the declaration file).
boolean	writeDeclaration(Declaration decl) Write declaration to declaration file.
java.io.File	writeProofIndex(Proof proof) Write index of proof to file suitable for later display of proof states.
java.io.File	writeProofState(ProofState state) Write proof state and return corresponding file.

Methods inherited from class java.lang.Object

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

Constructor Detail

Presenter

public Presenter(java.io.File directory)

Create instance of presenter with files in denoted directory.

Parameters:

directory - for storing the presentation files.

Method Detail

resize

public void resize()

Update font size depending on user settings.

newDeclarations

public boolean newDeclarations()

Creates new declaration document.

Returns:

true iff everything went well.

getDeclFile

public java.io.File getDeclFile()

Get file where all declarations are stored

Returns:

the declaration file

getFile

public java.io.File getFile(ProofState state)

Construct file name for proof state

Parameters:

state - the proof state.

Returns:

the name of the file for visualizing the proof state.

getRoot

public org.w3c.dom.Element getRoot(org.w3c.dom.Document document)

Get root node of document to which new nodes should be appended.

Parameters:

document - the document.

Returns:

its root node.

writeProofState

public java.io.File writeProofState(ProofState state)

Write proof state and return corresponding file.

Parameters:

state - the state to be written to file.

Returns:

the new file (null, if an error occured).

writeDeclaration

public boolean writeDeclaration(Declaration decl)

Write declaration to declaration file.

Parameters:

decl - the declaration to be written.

Returns:

true iff everything went okay.

updateDeclarations

public boolean updateDeclarations()

Update the declarations written so far (rewriting the declaration file). This is needed if the proof status of a formula (shown in display) has changed by a proof.

Returns:

true iff everything went okay.

writeProofIndex

public java.io.File writeProofIndex(Proof proof)

Write index of proof to file suitable for later display of proof states.

Parameters:

proof - the proof.

Returns:

file suitable for display (null, if an error occured)