001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010: package de.uka.ilkd.key.gui;
011:
012: import java.util.ArrayList;
013: import java.util.Collections;
014: import java.util.Iterator;
015: import java.util.List;
016:
017: import org.apache.log4j.Logger;
018:
019: import de.uka.ilkd.key.proof.*;
020:
021: public class KeYSelectionModel {
022:
023: /** the proof to listen to */
024: private Proof proof;
025: /** if true the selectedGoal field below can be trusted */
026: private boolean goalIsValid;
027: /** is the selected node a goal */
028: private Goal selectedGoal;
029: /** the current displayed node */
030: private Node selectedNode;
031: /** the listeners to this model */
032: private List listenerList;
033: /** cached selected node event */
034: private KeYSelectionEvent selectionEvent = new KeYSelectionEvent(
035: this );
036:
037: private Logger threadLogger = Logger.getLogger("key.threading");
038:
039: KeYSelectionModel() {
040: listenerList = Collections.synchronizedList(new ArrayList(5));
041: goalIsValid = false;
042: }
043:
044: /** sets the selected proof
045: * @param p the Proof that is selected
046: */
047: public void setSelectedProof(Proof p) {
048: goalIsValid = false;
049: proof = p;
050: if (proof != null) {
051: Goal g = proof.openGoals().iterator().next();
052: if (g == null) {
053: selectedNode = proof.root().leavesIterator().next();
054: } else {
055: goalIsValid = true;
056: selectedNode = g.node();
057: selectedGoal = g;
058: }
059: } else {
060: selectedNode = null;
061: selectedGoal = null;
062: }
063: fireSelectedProofChanged();
064: }
065:
066: /** returns the proof that is selected by the user
067: * @return the proof that is selected by the user
068: */
069: public Proof getSelectedProof() {
070: return proof;
071: }
072:
073: /** sets the node that is focused by the user
074: * @param n the selected node
075: */
076: public void setSelectedNode(Node n) {
077: goalIsValid = false;
078: selectedNode = n;
079: fireSelectedNodeChanged();
080: }
081:
082: /** sets the node that is focused by the user
083: * @param g the Goal that contains the selected node
084: */
085: public void setSelectedGoal(Goal g) {
086: goalIsValid = true;
087: selectedGoal = g;
088: selectedNode = g.node();
089: fireSelectedNodeChanged();
090: }
091:
092: /** returns the node that is selected by the user
093: * @return the node that is selected by the user
094: */
095: public Node getSelectedNode() {
096: return selectedNode;
097: }
098:
099: /** returns the goal the selected node belongs to, null if it is
100: * an inner node
101: * @return the goal the selected node belongs to, null if it is
102: * an inner node
103: */
104: public Goal getSelectedGoal() {
105: if (proof == null) {
106: throw new IllegalStateException("No proof loaded.");
107: }
108: if (!goalIsValid) {
109: selectedGoal = proof.getGoal(selectedNode);
110: goalIsValid = true;
111: }
112: return selectedGoal;
113: }
114:
115: /** returns true iff the selected node is a goal
116: * @return true iff the selected node is a goal
117: */
118: public boolean isGoal() {
119: if (!goalIsValid) {
120: return (getSelectedGoal() != null);
121: }
122: return selectedGoal != null;
123: }
124:
125: /** enumerate the possible goal selections, starting with the best
126: * one
127: */
128: protected class DefaultSelectionIterator implements IteratorOfGoal {
129: private static final int POS_START = 0;
130: private static final int POS_LEAVES = 1;
131: private static final int POS_GOAL_LIST = 2;
132:
133: private int currentPos = POS_START;
134: private Goal nextOne;
135: private IteratorOfGoal goalIt;
136: private IteratorOfNode nodeIt;
137:
138: public DefaultSelectionIterator() {
139: findNext();
140: }
141:
142: private void findNext() {
143: nextOne = null;
144: while (nextOne == null) {
145: switch (currentPos) {
146: case POS_START:
147: currentPos = POS_LEAVES;
148: if (selectedNode != null)
149: nodeIt = selectedNode.leavesIterator();
150: else
151: nodeIt = null;
152: break;
153: case POS_LEAVES:
154: if (nodeIt == null || !nodeIt.hasNext()) {
155: currentPos = POS_GOAL_LIST;
156: if (proof.openGoals() != SLListOfGoal.EMPTY_LIST)
157: goalIt = proof.openGoals().iterator();
158: else
159: goalIt = null;
160: } else
161: nextOne = proof.getGoal(nodeIt.next());
162: break;
163:
164: case POS_GOAL_LIST:
165: if (goalIt == null || !goalIt.hasNext())
166: // no more items
167: return;
168: else
169: nextOne = goalIt.next();
170: break;
171: }
172: }
173: }
174:
175: public Goal next() {
176: Goal res = nextOne;
177: findNext();
178: return res;
179: }
180:
181: public boolean hasNext() {
182: return nextOne != null;
183: }
184: }
185:
186: /** selectes the first goal in the goal list of proof if available
187: * if not it selectes a leaf of the proof tree
188: */
189: public void defaultSelection() {
190: Goal g = null;
191: Goal firstG = null;
192: IteratorOfGoal it = new DefaultSelectionIterator();
193:
194: while (g == null && it.hasNext()) {
195: g = it.next();
196: if (firstG == null)
197: firstG = g;
198: if (g.getClosureConstraint().isSatisfiable())
199: g = null;
200: }
201:
202: /** Order of preference:
203: * 1. Not yet closable goals
204: * 2. Goals which are not closed for all metavariable
205: * instantiations
206: * 3. The first node of the tree
207: */
208: if (g != null)
209: setSelectedGoal(g);
210: else {
211: if (firstG != null)
212: setSelectedGoal(firstG);
213: else
214: setSelectedNode(proof.root().leavesIterator().next());
215: }
216: /*
217: if (selectedNode != null) {
218: IteratorOfNode nodeIt = selectedNode.leavesIterator();
219: while (nodeIt.hasNext()) {
220: g = proof.getGoal(nodeIt.next());
221: if (g != null) {
222: break;
223: }
224: }
225: }
226: if (g == null && proof.openGoals() != SLListOfGoal.EMPTY_LIST ) {
227: g = proof.openGoals().iterator().next();
228: }
229: if (g != null) {
230: setSelectedGoal(g);
231: } else {
232: setSelectedNode(proof.root().leavesIterator().next());
233: }
234: */
235: }
236:
237: /**
238: * selects the first open goal below the given node <tt>old</tt>
239: * if no open goal is available node <tt>old</tt> is selected. In case
240: * that <tt>old</tt> has been removed from the proof the proof root is
241: * selected
242: * @param old the Node to start looking for open goals
243: */
244: public void nearestOpenGoalSelection(Node old) {
245: Node n = old;
246: while (n != null && n.isClosed()) {
247: n = n.parent();
248: }
249: if (n == null) {
250: if (proof.find(old)) {
251: setSelectedNode(old);
252: } else {
253: setSelectedNode(proof.root());
254: }
255: } else {
256: final Goal g = getFirstOpenGoalBelow(n);
257: if (g == null || g.node() == null) {
258: setSelectedNode(proof.root());
259: } else {
260: setSelectedGoal(g);
261: }
262: }
263: }
264:
265: /**
266: * retrievs the first open goal below the given node, i.e. the goal
267: * containing the first leaf of the subtree starting at
268: * <code>n</code> which is not already closed
269: *
270: * @param n the Node where to start from
271: * @return the goal containing the first leaf of the
272: * subtree starting at <code>n</code>, which is not already closed.
273: * <code>null</code> is returned if no such goal exists.
274: */
275: private Goal getFirstOpenGoalBelow(Node n) {
276: final IteratorOfNode it = n.leavesIterator();
277: while (it.hasNext()) {
278: final Node node = it.next();
279: if (!node.isClosed()) {
280: return proof.getGoal(node);
281: }
282: }
283: return null;
284: }
285:
286: public void addKeYSelectionListener(KeYSelectionListener listener) {
287: synchronized (listenerList) {
288: threadLogger.info("Adding " + listener.getClass());
289: listenerList.add(listener);
290: }
291: }
292:
293: public void removeKeYSelectionListener(KeYSelectionListener listener) {
294: synchronized (listenerList) {
295: threadLogger.info("Removing " + listener.getClass());
296: listenerList.remove(listener);
297: }
298: }
299:
300: public synchronized void fireSelectedNodeChanged() {
301: synchronized (listenerList) {
302: Iterator it = listenerList.iterator();
303: while (it.hasNext()) {
304: ((KeYSelectionListener) it.next())
305: .selectedNodeChanged(selectionEvent);
306: }
307: }
308: }
309:
310: public synchronized void fireSelectedProofChanged() {
311: synchronized (listenerList) {
312: threadLogger.info("Selected Proof changed, firing...");
313: Iterator it = listenerList.iterator();
314: while (it.hasNext()) {
315: ((KeYSelectionListener) it.next())
316: .selectedProofChanged(selectionEvent);
317: }
318: threadLogger.info("Selected Proof changed, done firing.");
319: }
320: }
321:
322: }
|