fmrisc.ProgramExplorer.InOut

Class Presenter

java.lang.Object

fmrisc.ProgramExplorer.InOut.Presenter

public final class Presenter
extends java.lang.Object

Interface to visual presentation of declarations and proof states.

Field Summary

Fields

Modifier and Type	Field and Description
static java.lang.String	detailId
static java.lang.String	detailName
static java.lang.String	detailName2
static java.lang.String	fileExt
static java.lang.String	methodId
static java.lang.String	methodName
static java.lang.String	nameFormStatAction
static java.lang.String	nameFormula
static java.lang.String	nameMethod
static java.lang.String	namePrePost
static java.lang.String	nameStatement
static java.lang.String	statPrefix
static java.lang.String	statPrefix2

Method Summary

Modifier and Type	Method and Description
static org.w3c.dom.Document	createDocument(java.lang.String title, int fontSize) Create new XHTML/MathML document.
static org.w3c.dom.Element	createTopNode(org.w3c.dom.Document document, int fontSize) Create top node for document content.
static VirtualDirectory	present(Formula formula, int fontSize, int width) Present formula in a certain font size.
static VirtualDirectory	present(ParamSymbol symbol, int fontSize, int width, int port) Present method in a certain font size.
static VirtualDirectory	present(ParamSymbol symbol, Statement statement, Formula formula, boolean pre, java.util.Map<Statement,Formula> preMap, java.util.Map<Statement,Formula> postMap, int fontSize, int width, int port) Present method in a certain font size.
void	setDetailFrame(java.lang.String file) Set detail frame of current frame to denoted file.
static void	writeDocument(org.w3c.dom.Document document, java.io.PrintWriter out) Write document to writer.
java.lang.String	writeStatement(Statement stat) Write file for statement and statement formula.

Methods inherited from class java.lang.Object

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

Field Detail

fileExt

public static final java.lang.String fileExt

See Also:

Constant Field Values

methodId

public static final java.lang.String methodId

See Also:

Constant Field Values

detailId

public static final java.lang.String detailId

See Also:

Constant Field Values

methodName

public static final java.lang.String methodName

See Also:

Constant Field Values

detailName

public static final java.lang.String detailName

See Also:

Constant Field Values

detailName2

public static final java.lang.String detailName2

See Also:

Constant Field Values

statPrefix

public static final java.lang.String statPrefix

See Also:

Constant Field Values

statPrefix2

public static final java.lang.String statPrefix2

See Also:

Constant Field Values

nameFormStatAction

public static final java.lang.String nameFormStatAction

See Also:

Constant Field Values

nameMethod

public static final java.lang.String nameMethod

See Also:

Constant Field Values

nameStatement

public static final java.lang.String nameStatement

See Also:

Constant Field Values

nameFormula

public static final java.lang.String nameFormula

See Also:

Constant Field Values

namePrePost

public static final java.lang.String namePrePost

See Also:

Constant Field Values

Method Detail

present

public static VirtualDirectory present(ParamSymbol symbol,
                                       int fontSize,
                                       int width,
                                       int port)

Present method in a certain font size.

Parameters:

symbol - the symbol of the method.

fontSize - the font size.

width - the number of characters per line to be used for the detail view.

port - the port number of the command server.

Returns:

a directory whose main file contains the output (the file may contain links to other files in the directory).

present

public static VirtualDirectory present(Formula formula,
                                       int fontSize,
                                       int width)

Present formula in a certain font size.

Parameters:

formula - the formula.

fontSize - the font size.

width - the number of characters per line to be used

Returns:

a directory whose main file contains the output (the file may contain links to other files in the directory).

present

public static VirtualDirectory present(ParamSymbol symbol,
                                       Statement statement,
                                       Formula formula,
                                       boolean pre,
                                       java.util.Map<Statement,Formula> preMap,
                                       java.util.Map<Statement,Formula> postMap,
                                       int fontSize,
                                       int width,
                                       int port)

Present method in a certain font size.

Parameters:

symbol - the symbol of the method.

statement - the statement.

formula - the formula.

pre - true iff formula is precondition.

preMap - the precondition map.

postMap - the postcondition map.

fontSize - the font size.

width - the number of characters per line to be used for the detail view.

port - the port number of the command server.

Returns:

a directory whose main file contains the output (the file may contain links to other files in the directory).

setDetailFrame

public void setDetailFrame(java.lang.String file)

Set detail frame of current frame to denoted file.

Parameters:

file - the denoted file.

writeStatement

public java.lang.String writeStatement(Statement stat)

Write file for statement and statement formula.

Parameters:

stat - the statement to be written

Returns:

the name of the file

createDocument

public static org.w3c.dom.Document createDocument(java.lang.String title,
                                                  int fontSize)

Create new XHTML/MathML document.

Parameters:

title - the document title

fontSize - the font size

Returns:

the new document

createTopNode

public static org.w3c.dom.Element createTopNode(org.w3c.dom.Document document,
                                                int fontSize)

Create top node for document content.

Parameters:

document - the document.

fontSize - the font size

Returns:

the node to which to append content.

writeDocument

public static void writeDocument(org.w3c.dom.Document document,
                                 java.io.PrintWriter out)

Write document to writer.

Parameters:

document - the document.

out - the writer.