fmrisc.ProofNavigator.Commands
Class ProofCommandBase

java.lang.Object
  fmrisc.ProofNavigator.Commands.CommandBase
      fmrisc.ProofNavigator.Commands.ProofCommandBase

All Implemented Interfaces:

Command, ProofCommand

Direct Known Subclasses:

Assume, Auto, AutoStar, Case, CounterExample, Decompose, Expand, Flatten, Flip, Goal, Goto, Induction, Instantiate, Lemma, Next, Open, Option, Prev, Proved, Redo, Scatter, Simplify, Skolemize, Split, TypeAxiom, Undo

public abstract class ProofCommandBase
extends CommandBase
implements ProofCommand

Base class of proof commands.

Constructor Summary

ProofCommandBase(java.lang.String name)
construct proof command with denoted name.

Method Summary

void	process() apply command to current state of current proof.
ProofState[]	process(ProofState state) process proof state (in environment denoted by that state).

Methods inherited from class fmrisc.ProofNavigator.Commands.CommandBase

getName, printCore, toCommand, toNode, toString

Methods inherited from class java.lang.Object

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

Methods inherited from interface fmrisc.ProofNavigator.Commands.Command

toNode

Constructor Detail

ProofCommandBase

public ProofCommandBase(java.lang.String name)

construct proof command with denoted name.

Parameters:

name - the name of the proof command

Method Detail

process

public final ProofState[] process(ProofState state)

process proof state (in environment denoted by that state). This function rather than processCore() must be called by any proof command that wishes to execute another proof command.

Specified by:

process in interface ProofCommand

Parameters:

state - the state to which the proof command is applied (remains unchanged)

Returns:

a sequence of children of state generated by the command (null, if the command did not generate any)

process

public void process()

apply command to current state of current proof.

Specified by:

process in interface Command