public class TacletFindModel
extends javax.swing.table.AbstractTableModel
Modifier and Type | Field and Description |
---|---|
private java.util.ArrayList<Pair<SchemaVariable,java.lang.String>> |
entries
the instantiations entries
|
private Goal |
goal
the current goal
|
private InstantiationProposerCollection |
instantiationProposers
proposers to ask when instantiating a schema variable
|
private int |
noEditRow
the integer defines the row until which no editing is possible
|
private NamespaceSet |
nss
universal namespace of variables, minimum for input in a row
|
private TacletApp |
originalApp
the related rule application
|
private AbbrevMap |
scm
the abbreviation map
|
private static long |
serialVersionUID |
private Services |
services
the java service object
|
private VariableNamer |
varNamer
variable namer
|
Constructor and Description |
---|
TacletFindModel(TacletApp app,
Services services,
NamespaceSet nss,
AbbrevMap scm,
Goal goal)
create new data model for tree
|
Modifier and Type | Method and Description |
---|---|
private void |
checkNeededInputAvailable(int irow)
throws an exception iff no input in indicated row, and no
metavariable instantiation is possible
|
private java.util.ArrayList<Pair<SchemaVariable,java.lang.String>> |
createEntryArray(TacletApp tacletApp)
creates a Vector with the row entries of the table
|
TacletApp |
createTacletAppFromVarInsts()
creates new rule app with all inserted instantiations in the variable
instantiations table
|
int |
getColumnCount()
number of columns
|
int |
getRowCount()
number of rows
|
private int |
getSVRow(SchemaVariable sv)
returns the index of the row the given Schemavariable stands
|
java.lang.Object |
getValueAt(int row,
int col)
get value at the specified row and col
|
boolean |
isCellEditable(int rowIndex,
int columnIndex)
returns true iff an instantiation is missing
|
private boolean |
isInputAvailable(int irow) |
private NamespaceSet |
namespaces()
returns the set of namespaces
|
private IdDeclaration |
parseIdDeclaration(int irow)
parses the indicated row and returns a identifier declaration
corresponding to the entry in the row
|
private IdDeclaration |
parseIdDeclaration(java.lang.String s)
Parse the declaration of an identifier (i.e. the declaration of
a variable or skolem function)
|
private ProgramElement |
parseRow(int irow)
parses the indicated row and returns the ProgramElement
corresponding to the entry in the row
|
private Term |
parseRow(int irow,
Namespace<QuantifiableVariable> varNS,
Namespace<Function> functNS)
parses the indicated row and returns a Term corresponding to the
entry in the row
|
private Term |
parseTerm(java.lang.String s,
Namespace<QuantifiableVariable> varNS,
Namespace<Function> functNS)
parses the given string that represents the term (or formula)
using the given variable namespace and the given namespace
for functions and default namespaces for the others
|
void |
setValueAt(java.lang.Object instantiation,
int rowIndex,
int columnIndex)
sets the value of the cell
|
addTableModelListener, findColumn, fireTableCellUpdated, fireTableChanged, fireTableDataChanged, fireTableRowsDeleted, fireTableRowsInserted, fireTableRowsUpdated, fireTableStructureChanged, getColumnClass, getColumnName, getListeners, getTableModelListeners, removeTableModelListener
private static final long serialVersionUID
private java.util.ArrayList<Pair<SchemaVariable,java.lang.String>> entries
private final TacletApp originalApp
private int noEditRow
private NamespaceSet nss
private Services services
private AbbrevMap scm
private Goal goal
private VariableNamer varNamer
private InstantiationProposerCollection instantiationProposers
public TacletFindModel(TacletApp app, Services services, NamespaceSet nss, AbbrevMap scm, Goal goal)
app
- the TacletApp where to get the necessary entriesprivate NamespaceSet namespaces()
private java.util.ArrayList<Pair<SchemaVariable,java.lang.String>> createEntryArray(TacletApp tacletApp)
public int getColumnCount()
public int getRowCount()
public boolean isCellEditable(int rowIndex, int columnIndex)
isCellEditable
in interface javax.swing.table.TableModel
isCellEditable
in class javax.swing.table.AbstractTableModel
private Term parseTerm(java.lang.String s, Namespace<QuantifiableVariable> varNS, Namespace<Function> functNS) throws ParserException
s
- the String to parsevarNS
- the variable namespacefunctNS
- the function namespaceParserException
private IdDeclaration parseIdDeclaration(java.lang.String s) throws ParserException
ParserException
private void checkNeededInputAvailable(int irow) throws MissingInstantiationException
MissingInstantiationException
private boolean isInputAvailable(int irow)
private Term parseRow(int irow, Namespace<QuantifiableVariable> varNS, Namespace<Function> functNS) throws SVInstantiationParserException, MissingInstantiationException
irow
- the row to be parsedvarNS
- the variable namespace that will be passed to parseTermfunctNS
- the function namespace that will be passed to parseTermSVInstantiationParserException
MissingInstantiationException
private IdDeclaration parseIdDeclaration(int irow) throws SVInstantiationParserException, MissingInstantiationException
irow
- the row to be parsedSVInstantiationParserException
MissingInstantiationException
private ProgramElement parseRow(int irow) throws SVInstantiationParserException
irow
- the row to be parsedSVInstantiationParserException
public TacletApp createTacletAppFromVarInsts() throws SVInstantiationException
SVInstantiationException
- if the instantiation is incorrectpublic void setValueAt(java.lang.Object instantiation, int rowIndex, int columnIndex)
setValueAt
in interface javax.swing.table.TableModel
setValueAt
in class javax.swing.table.AbstractTableModel
public java.lang.Object getValueAt(int row, int col)
private int getSVRow(SchemaVariable sv)