| java.lang.Object javax.swing.table.AbstractTableModel de.uka.ilkd.key.proof.TacletInstantiationsTableModel
Method Summary | |
public void | addInstantiationEntry(int row, Term instantiation) | public TacletApp | application() | public TacletApp | createTacletAppFromVarInsts() | public int | getColumnCount() | public static String | getNameProposalForMetavariable(Goal goal, TacletApp p_app, SchemaVariable p_var) | public static ProgramElement | getProgramElement(TacletApp app, String instantiation, SchemaVariable sv, Services services) | public int | getRowCount() | public int | getSVRow(SchemaVariable sv) | public Object | getValueAt(int row, int col) | public boolean | isCellEditable(int rowIndex, int columnIndex) | public NamespaceSet | namespaces() | public IdDeclaration | parseIdDeclaration(String s) Parse the declaration of an identifier (i.e. | public Term | parseTerm(String s, Namespace varNS) | public void | setValueAt(Object instantiation, int rowIndex, int columnIndex) |
TacletInstantiationsTableModel | public TacletInstantiationsTableModel(TacletApp app, Services services, NamespaceSet nss, AbbrevMap scm, Goal goal)(Code) | | create new data model for tree
Parameters: app - the TacletApp where to get the necessary entries |
addInstantiationEntry | public void addInstantiationEntry(int row, Term instantiation)(Code) | | adds an instantiation of a schemavariable
|
application | public TacletApp application()(Code) | | return the rule application which is the table models base
the Ruleapp |
getColumnCount | public int getColumnCount()(Code) | | number of colums
number of colums |
getRowCount | public int getRowCount()(Code) | | number of rows
number of rows |
getSVRow | public int getSVRow(SchemaVariable sv)(Code) | | returns the index of the row the given Schemavariable stands
the index of the row the given Schemavariable stands (-1if not found) |
getValueAt | public Object getValueAt(int row, int col)(Code) | | get value at the specified row and col
the value |
isCellEditable | public boolean isCellEditable(int rowIndex, int columnIndex)(Code) | | returns true iff an instantiation is missing
true iff an instantiation is missing |
parseTerm | public Term parseTerm(String s, Namespace varNS) throws ParserException(Code) | | parses the given string that represents the term (or formula)
using the given variable namespace and the default namespaces
for functions and sorts
Parameters: s - the String to parse Parameters: sort - the expected sort Parameters: varNS - the variable namespace |
setValueAt | public void setValueAt(Object instantiation, int rowIndex, int columnIndex)(Code) | | sets the Value of the cell
|
|
|