fmrisc.ProofNavigator.Commands
Class Redo

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

All Implemented Interfaces:

Command, ProofCommand

public final class Redo
extends ProofCommandBase

The "redo" command: goto an open proof state and redo its proof.

Field Summary

static java.lang.String

Name

Constructor Summary

Redo(java.lang.String label)
create a "redo" command

Method Summary

void	printCore(java.io.PrintWriter out) Prints text representation on out (without new line termination).

Methods inherited from class fmrisc.ProofNavigator.Commands.ProofCommandBase

process, process

Methods inherited from class fmrisc.ProofNavigator.Commands.CommandBase

getName, 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

Field Detail

Name

public static final java.lang.String Name

See Also:

Constant Field Values

Constructor Detail

Redo

public Redo(java.lang.String label)

create a "redo" command

Parameters:

label - the label of the proof state to go to (may be null)

Method Detail

printCore

public void printCore(java.io.PrintWriter out)

Prints text representation on out (without new line termination).

Specified by:

printCore in class CommandBase

Parameters:

out - the stream on which the text is written