fmrisc.ProofNavigator
Class Main

java.lang.Object
  fmrisc.ProofNavigator.Main

public final class Main
extends java.lang.Object

Command line interface to ProofNavigator.

Constructor Summary

Main()

Method Summary

static boolean	ask(java.lang.String question) Ask question to be answered by user with 'y' or 'n'
static void	displayDeclarations() Signal that declarations are to be displayed.
static void	exit(int code) Terminate program with denoted exit code.
static java.lang.String	getVersion() Return version string.
static void	init() Initialize the system state.
static boolean	isRunning() Signal whether command is being processed.
static void	main(java.lang.String[] args) Command line interface to ProofNavigator.
static boolean	newDeclaration(Declaration decl) Signal new declaration.
static boolean	open(java.lang.String path) Read command from file with denoted path.
static Command	parse() Parse next command.
static void	quit() Quit (session or current proof) after asking user whether to do so.
static java.lang.String	readLine() Read line of input from console.
static void	resetProof() Signal there is no current proof.
static void	run() Run ProofNavigator interpreter.
static boolean	setContext(java.lang.String path) Set context directory.
static void	setProof(Proof proof) Signal current proof.
static void	setProofState(ProofState state) Signal current proof state.

Methods inherited from class java.lang.Object

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

Constructor Detail

Main

public Main()

Method Detail

main

public static void main(java.lang.String[] args)

Command line interface to ProofNavigator.

Parameters:

args - empty or file to be read upon startup

getVersion

public static java.lang.String getVersion()

Return version string.

init

public static void init()

Initialize the system state.

run

public static void run()

Run ProofNavigator interpreter. Assumes that input/output interface has been initialized.

parse

public static Command parse()

Parse next command.

Returns:

next command parsed (null, if a syntax error occured).

exit

public static void exit(int code)

Terminate program with denoted exit code.

Parameters:

code - the exit code

quit

public static void quit()

Quit (session or current proof) after asking user whether to do so. Saves the proof in current store, if this is what the user wants.

readLine

public static java.lang.String readLine()

Read line of input from console.

Returns:

the line (null, if an error occured)

ask

public static boolean ask(java.lang.String question)

Ask question to be answered by user with 'y' or 'n'

Parameters:

question - the question asked

Returns:

true iff answer was 'y'

setProof

public static void setProof(Proof proof)

Signal current proof.

Parameters:

proof - the current proof

resetProof

public static void resetProof()

Signal there is no current proof.

setProofState

public static void setProofState(ProofState state)

Signal current proof state.

Parameters:

state - the current proof state.

newDeclaration

public static boolean newDeclaration(Declaration decl)

Signal new declaration.

Parameters:

decl - the new declaration.

Returns:

true iff everything went okay.

displayDeclarations

public static void displayDeclarations()

Signal that declarations are to be displayed.

open

public static boolean open(java.lang.String path)

Read command from file with denoted path.

Parameters:

path - the (absolute or relative) path to the file.

Returns:

true iff everything went okay.

setContext

public static boolean setContext(java.lang.String path)

Set context directory.

Parameters:

path - the (absolute or relative) path to context directory (if null, a default path is used).

Returns:

true iff everything went okay.

isRunning

public static boolean isRunning()

Signal whether command is being processed.

Returns:

true iff command is being processed.