public class TacletAssumesModel extends javax.swing.DefaultComboBoxModel<IfFormulaInstantiation>
Modifier and Type | Field and Description |
---|---|
private Term |
ifFma |
private java.lang.String |
manualInput |
private static IfFormulaInstantiation |
manualTextIF |
private NamespaceSet |
nss
namespaces (variables, functions, sorts, etc.)
|
private AbbrevMap |
scm |
private static long |
serialVersionUID
generated UID
|
private Services |
services |
Constructor and Description |
---|
TacletAssumesModel(Term p_ifFma,
ImmutableList<IfFormulaInstantiation> p_candidates,
Services p_services,
NamespaceSet nss,
AbbrevMap scm) |
Modifier and Type | Method and Description |
---|---|
static IfFormulaInstantiation[] |
createIfInsts(ImmutableList<IfFormulaInstantiation> p_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) |
private KeYParserF |
stringParser(java.lang.String s)
creates a new Termparser that parses the given string
|
addElement, getElementAt, getIndexOf, getSelectedItem, getSize, insertElementAt, removeAllElements, removeElement, removeElementAt, setSelectedItem
addListDataListener, fireContentsChanged, fireIntervalAdded, fireIntervalRemoved, getListDataListeners, getListeners, removeListDataListener
private static final long serialVersionUID
private static final IfFormulaInstantiation manualTextIF
private java.lang.String manualInput
private final Term ifFma
private final NamespaceSet nss
private final AbbrevMap scm
private final Services services
public TacletAssumesModel(Term p_ifFma, ImmutableList<IfFormulaInstantiation> p_candidates, Services p_services, NamespaceSet nss, AbbrevMap scm)
public void setInput(java.lang.String s)
public Term ifFma()
public static IfFormulaInstantiation[] createIfInsts(ImmutableList<IfFormulaInstantiation> p_candidates)
private KeYParserF stringParser(java.lang.String s)
s
- the String to parsepublic Term parseFormula(java.lang.String s) throws org.antlr.runtime.RecognitionException
s
- the String to parseorg.antlr.runtime.RecognitionException
- In case an exceptions 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()