public class TacletInstantiationModel
extends java.lang.Object
Constructor and Description |
---|
TacletInstantiationModel(TacletApp app,
Sequent seq,
NamespaceSet nss,
AbbrevMap scm,
Goal goal)
Create new data model for the apply Taclet dialog wrapping a combo box model
and a table model.
|
Modifier and Type | Method and Description |
---|---|
void |
addModelChangeListener(ModelChangeListener l) |
TacletApp |
application() |
TacletApp |
createTacletApp() |
Services |
getServices()
Gets the services in use by this object.
|
java.lang.String |
getStatusString() |
TacletAssumesModel |
ifChoiceModel(int i) |
int |
ifChoiceModelCount() |
Term |
ifFma(int i) |
void |
prepareUnmatchedInstantiation()
replaces the TacletApp of this ApplyTacletDialogModel by an TacletApp where
all name conflicts are resolved and thus the parser is enabled to accept
variables from the context or the prefix of the Taclet.
|
Namespace<IProgramVariable> |
programVariables() |
Proof |
proof() |
void |
removeModelChangeListener(ModelChangeListener l) |
void |
setManualInput(int i,
java.lang.String s)
sets the manual if-input
|
TacletFindModel |
tableModel() |
Taclet |
taclet() |
TacletApp |
tacletApp() |
public TacletInstantiationModel(TacletApp app, Sequent seq, NamespaceSet nss, AbbrevMap scm, Goal goal)
app
- seq
- nss
- scm
- goal
- public void addModelChangeListener(ModelChangeListener l)
public void removeModelChangeListener(ModelChangeListener l)
public TacletAssumesModel ifChoiceModel(int i)
public int ifChoiceModelCount()
public TacletFindModel tableModel()
public TacletApp application()
public Taclet taclet()
public TacletApp tacletApp()
public Proof proof()
public Term ifFma(int i)
public java.lang.String getStatusString()
public TacletApp createTacletApp() throws SVInstantiationException
SVInstantiationException
public void setManualInput(int i, java.lang.String s)
public void prepareUnmatchedInstantiation()
public Namespace<IProgramVariable> programVariables()
public Services getServices()
Copyright © 2003-2019 The KeY-Project.