public class TacletAssumesModel extends javax.swing.DefaultComboBoxModel<IfFormulaInstantiation>
Constructor and Description |
---|
TacletAssumesModel(Term ifFma,
ImmutableList<IfFormulaInstantiation> candidates,
TacletApp app,
Goal goal,
Services services,
NamespaceSet nss,
AbbrevMap scm) |
Modifier and Type | Method and Description |
---|---|
static IfFormulaInstantiation[] |
createIfInsts(ImmutableList<IfFormulaInstantiation> candidates) |
IfFormulaInstantiation |
getSelection(int pos) |
Term |
ifFma() |
boolean |
isManualInputSelected() |
Term |
parseFormula(java.lang.String s)
parses and returns the term encoded as string 's'
|
void |
setInput(java.lang.String s) |
addElement, getElementAt, getIndexOf, getSelectedItem, getSize, insertElementAt, removeAllElements, removeElement, removeElementAt, setSelectedItem
addListDataListener, fireContentsChanged, fireIntervalAdded, fireIntervalRemoved, getListDataListeners, getListeners, removeListDataListener
public TacletAssumesModel(Term ifFma, ImmutableList<IfFormulaInstantiation> candidates, TacletApp app, Goal goal, Services services, NamespaceSet nss, AbbrevMap scm)
public void setInput(java.lang.String s)
public Term ifFma()
public static IfFormulaInstantiation[] createIfInsts(ImmutableList<IfFormulaInstantiation> candidates)
public Term parseFormula(java.lang.String s) throws org.antlr.runtime.RecognitionException
s
- the String to parseorg.antlr.runtime.RecognitionException
- In case an exception occurs during parse.public IfFormulaInstantiation getSelection(int pos) throws SVInstantiationParserException, MissingInstantiationException
pos
- int describes position of the if-sequent (only required for error
message)SVInstantiationParserException
MissingInstantiationException
public boolean isManualInputSelected()
Copyright © 2003-2019 The KeY-Project.