public class TacletInstantiationModel
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
private TacletApp |
app
the application of the Taclet of which this model is used to
complete the instantiations of the schemavariables and/or
if-sequent
|
private ModelEvent |
changeEvent
the change event that is sent
|
private static TacletAssumesModel[] |
EMPTY_IF_CHOICES |
private TacletAssumesModel[] |
ifChoiceModel
the model used for the instantiation of the if-sequent
|
private java.util.Vector<ModelChangeListener> |
listeners
listeners of this model
|
private NamespaceSet |
nss
namespace of variables
|
private Proof |
proof |
private AbbrevMap |
scm |
private Sequent |
seq
the sequent the application above is applied
|
private Services |
services |
private TacletFindModel |
tableModel
the model used for the instantiation of the schemavariables
|
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() |
private TacletApp |
createTacletAppFromIfs(TacletApp tacletApp) |
Services |
getServices()
Gets the services in use by this object.
|
java.lang.String |
getStatusString() |
TacletAssumesModel |
ifChoiceModel(int i) |
int |
ifChoiceModelCount() |
Term |
ifFma(int i) |
private void |
informListenerAboutModelChange() |
private void |
initIfChoiceModels() |
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() |
private TacletAssumesModel[] ifChoiceModel
private static final TacletAssumesModel[] EMPTY_IF_CHOICES
private final TacletFindModel tableModel
private TacletApp app
private final Sequent seq
private final java.util.Vector<ModelChangeListener> listeners
private final ModelEvent changeEvent
private final NamespaceSet nss
private final Services services
private final AbbrevMap scm
private final Proof proof
public TacletInstantiationModel(TacletApp app, Sequent seq, NamespaceSet nss, AbbrevMap scm, Goal 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)
private void initIfChoiceModels()
private TacletApp createTacletAppFromIfs(TacletApp tacletApp) throws IfMismatchException, SVInstantiationParserException, MissingInstantiationException, SortMismatchException
public java.lang.String getStatusString()
public TacletApp createTacletApp() throws SVInstantiationException
SVInstantiationException
private void informListenerAboutModelChange()
public void setManualInput(int i, java.lang.String s)
public void prepareUnmatchedInstantiation()
public Namespace<IProgramVariable> programVariables()
public Services getServices()