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: // This file is part of KeY - Integrated Deductive Software Design
010: // Copyright (C) 2001-2004 Universitaet Karlsruhe, Germany
011: // Universitaet Koblenz-Landau, Germany
012: // Chalmers University of Technology, Sweden
013: //
014: // The KeY system is protected by the GNU General Public License.
015: // See LICENSE.TXT for details.
016: package de.uka.ilkd.key.gui.assistant;
017:
018: import java.awt.Component;
019: import java.awt.Container;
020: import java.awt.event.*;
021: import java.util.Iterator;
022: import java.util.LinkedList;
023: import java.util.List;
024:
025: import javax.swing.AbstractButton;
026: import javax.swing.event.ChangeEvent;
027: import javax.swing.event.ChangeListener;
028: import javax.swing.event.EventListenerList;
029:
030: import de.uka.ilkd.key.gui.*;
031: import de.uka.ilkd.key.gui.configuration.GeneralSettings;
032: import de.uka.ilkd.key.gui.configuration.SettingsListener;
033: import de.uka.ilkd.key.proof.ProofEvent;
034: import de.uka.ilkd.key.rule.RuleApp;
035:
036: /**
037: * The proof assistant controller is connected to several system
038: * points. The events send from these points are passed through to the
039: * AI which decides about the actions to be executed.
040: */
041: public class ProofAssistantController {
042:
043: /**
044: * the mediator
045: */
046: private KeYMediator mediator;
047:
048: /**
049: * the artificial intelligence to be informed about occured events
050: */
051: private ProofAssistantAI assistantAI;
052:
053: /**
054: * true if the assistant is activated
055: */
056: private boolean enabled;
057:
058: /**
059: * true if the assistant is tentaive
060: */
061: private boolean registered;
062:
063: /** listens to events sent by the prover */
064: private AIProofListener proofListener;
065:
066: /** listens to events sent by the toolbar */
067: private AIToolBarListener toolBarListener;
068:
069: /** listens to events sent by the menu bar */
070: private AIMenuBarListener menuBarListener;
071:
072: /**
073: * listens to events such as changing the selected node or proof
074: */
075: private AIKeYSelectionListener selectionListener;
076:
077: /** the frame object encapsulating the assistant pane */
078: private ProofAssistant assistantGUI;
079:
080: /**
081: * list containing the listeners of the assistant
082: */
083: private EventListenerList listeners = new EventListenerList();
084:
085: /**
086: * runnables to register the AI
087: */
088: private Runnable registerCtrl = new Runnable() {
089: public void run() {
090: ProofAssistantController.this .register();
091: }
092: };
093:
094: /**
095: * runnables to unregister the AI
096: */
097: private Runnable unregisterCtrl = new Runnable() {
098: public void run() {
099: ProofAssistantController.this .unregister();
100: }
101: };
102:
103: /**
104: * creates the proof assistant controller associated with the
105: * given AI.
106: * @param mediator the KeYMediator
107: * @param settings the GenberalSettings indicating if the
108: * assistant should be enabled or disabled
109: * @param ai the ProofAssistantAI
110: * @param ui the ProofAssistant user interface
111: */
112: public ProofAssistantController(KeYMediator mediator,
113: GeneralSettings settings, ProofAssistantAI ai,
114: ProofAssistant ui) {
115:
116: this .mediator = mediator;
117: settings.addSettingsListener(new AISettingsListener());
118: assistantAI = ai;
119: assistantGUI = ui;
120:
121: assistantGUI
122: .addWindowListener(new ProofAssistantWindowListener());
123:
124: init((Main) mediator.mainFrame());
125:
126: if (settings.proofAssistantMode()) {
127: enable();
128: } else {
129: disable();
130: }
131: }
132:
133: /**
134: * initialize the controller
135: */
136: private void init(Main mainFrame) {
137: proofListener = new AIProofListener();
138: selectionListener = new AIKeYSelectionListener();
139:
140: toolBarListener = new AIToolBarListener(mainFrame.getToolBar());
141: mainFrame.getToolBar().addContainerListener(toolBarListener);
142:
143: menuBarListener = new AIMenuBarListener(mainFrame.getJMenuBar());
144: mainFrame.getJMenuBar().addContainerListener(menuBarListener);
145:
146: final int width = mainFrame.getGraphicsConfiguration()
147: .getDevice().getDisplayMode().getWidth();
148:
149: assistantGUI.setLocation(width - assistantGUI.getWidth(), 0);
150: }
151:
152: /**
153: * enables the assistant
154: */
155: public void enable() {
156: if (enabled)
157: return;
158: if (!registered)
159: register();
160: // we have to register and stay registered as interactive
161: // proof listener as long as AI is enabled
162: registerAtInteractiveProver();
163: assistantGUI.tearUp();
164: enabled = true;
165: fireStateChangeEvent();
166: }
167:
168: /**
169: * disables the assistant
170: */
171: public void disable() {
172: if (!enabled)
173: return;
174: if (registered)
175: unregister();
176: unregisterAtInteractiveProver();
177: assistantGUI.tearDown();
178: enabled = false;
179: fireStateChangeEvent();
180: }
181:
182: /**
183: * Registers the controller at the interactive prover in
184: * order. If in automatic application mode, we can unregister
185: * all listeners, but not the interactive prover
186: * listener. Otherwise we would miss the event that the auto mode
187: * has stopped,
188: */
189: private void registerAtInteractiveProver() {
190: mediator.addRuleAppListener(proofListener);
191: mediator.addAutoModeListener(proofListener);
192: }
193:
194: /**
195: * Registers the controller at the toolbar. The way this is done
196: * is not nice at the moment, but we need a redesign of GUI to
197: * realize it in a more convenient way.
198: */
199: private void registerAtToolBar() {
200: toolBarListener.registerAll();
201: }
202:
203: /**
204: * Registers the controller at the menubar. The way this is done
205: * is not nice at the moment, but we need a redesign of GUI to
206: * realize it in a more convenient way.
207: */
208: private void registerAtMenuBar() {
209: menuBarListener.registerAll();
210: }
211:
212: /**
213: * Unregisters the controller at the interactive prover in
214: * order. If in automatic application mode, we can unregister
215: * all listeners, but not the interactive prover
216: * listener. Otherwise we would miss the event that the auto mode
217: * has stopped,
218: */
219: private void unregisterAtInteractiveProver() {
220: mediator.removeRuleAppListener(proofListener);
221: mediator.removeAutoModeListener(proofListener);
222: }
223:
224: /**
225: * Unregisters the controller at the toolbar.
226: */
227: private void unregisterAtToolBar() {
228: toolBarListener.unregisterAll();
229: }
230:
231: /**
232: * Unregisters the controller at the menubar. The way this is done
233: * is not nice at the moment, but we need a redesign of GUI to
234: * realize it in a more convenient way.
235: */
236: private void unregisterAtMenuBar() {
237: menuBarListener.unregisterAll();
238: }
239:
240: /**
241: * registers at all observed system points
242: */
243: private void register() {
244: if (registered)
245: return;
246: mediator.addKeYSelectionListener(selectionListener);
247: registerAtToolBar();
248: registerAtMenuBar();
249: registered = true;
250: }
251:
252: /**
253: * unregisters at all observed system points except at the
254: * interactive prover
255: */
256: private void unregister() {
257: if (!registered)
258: return;
259: mediator.removeKeYSelectionListener(selectionListener);
260: unregisterAtToolBar();
261: unregisterAtMenuBar();
262: registered = false;
263: }
264:
265: /**
266: * the given text is displayed by the assistant
267: */
268: public void displayText(String text) {
269: if (assistantGUI != null) {
270: assistantGUI.setText(text);
271: }
272: }
273:
274: /**
275: * returns the state of the assistant (true means enabled, false
276: * disabled)
277: */
278: public boolean getState() {
279: return enabled;
280: }
281:
282: /**
283: * adds a change listener to this assistant
284: * @param l the ChangeListener
285: */
286: public void addChangeListener(ChangeListener l) {
287: listeners.add(ChangeListener.class, l);
288: }
289:
290: /**
291: * removes the giben change listener from this assistant
292: * @param l the ChangeListener
293: */
294: public void removeChangeListener(ChangeListener l) {
295: listeners.remove(ChangeListener.class, l);
296: }
297:
298: /**
299: * fire state change event
300: */
301: private void fireStateChangeEvent() {
302: Object[] listenersArray = listeners.getListenerList();
303: for (int i = listenersArray.length - 2; i >= 0; i -= 2) {
304: if (listenersArray[i] == ChangeListener.class) {
305: ((ChangeListener) listenersArray[i + 1])
306: .stateChanged(new ChangeEvent(this ));
307: }
308: }
309: }
310:
311: // the window adapter to observer the GUI
312: private class ProofAssistantWindowListener extends WindowAdapter {
313:
314: public void windowClosing(WindowEvent we) {
315: ProofAssistantController.this .disable();
316: }
317:
318: }
319:
320: // The different listeners connecting to the system points
321:
322: /**
323: * This abstract container listener can be subclassed if a
324: * listener needs to be registered to all components of a
325: * container.
326: */
327: private abstract class AIContainerListener implements
328: ContainerListener {
329:
330: private List components = new LinkedList();
331:
332: public abstract void register(Component c);
333:
334: public abstract void unregister(Component c);
335:
336: public AIContainerListener(Container container) {
337: init(container);
338: }
339:
340: /**
341: * collects at all components of the given container and puts
342: * them in the observed list
343: */
344: private void init(Container container) {
345: Component[] comps = container.getComponents();
346: for (int i = 0; i < comps.length; i++) {
347: components.add(comps[i]);
348: }
349: }
350:
351: /**
352: * registers at the added component and adds it to the list of
353: * observed components
354: */
355: public void componentAdded(ContainerEvent ce) {
356: register(ce.getChild());
357: components.add(ce.getChild());
358: }
359:
360: /**
361: * unregisters at the added component and removes it from the list of
362: * observed components
363: */
364: public void componentRemoved(ContainerEvent ce) {
365: unregister(ce.getChild());
366: components.remove(ce.getChild());
367: }
368:
369: /**
370: * registers all observed components
371: */
372: public void registerAll() {
373: synchronized (components) {
374: Iterator it = components.iterator();
375: while (it.hasNext()) {
376: register((Component) it.next());
377: }
378: }
379: }
380:
381: /**
382: * unregisters all observed components, but keeps them in the
383: * observed component list
384: */
385: public void unregisterAll() {
386: synchronized (components) {
387: Iterator it = components.iterator();
388: while (it.hasNext()) {
389: unregister((Component) it.next());
390: }
391: }
392: }
393:
394: }
395:
396: /**
397: * This listener listens to toolbar events. %%%
398: * The GUI needs to be redesigned then the implementation of this
399: * listener could be nicer, but in the meantime.
400: */
401: private class AIToolBarListener extends AIContainerListener
402: implements ActionListener {
403:
404: private ProofAssistantController ctrl = ProofAssistantController.this ;
405:
406: public AIToolBarListener(Container container) {
407: super (container);
408: }
409:
410: public void actionPerformed(ActionEvent e) {
411: if (e.getSource() instanceof AbstractButton) {
412: ctrl.assistantAI.analyze(
413: new PressedButtonEventInput((AbstractButton) e
414: .getSource(), AIInput.TOOLBAR_EVENT))
415: .execute(ctrl);
416: }
417: }
418:
419: public void register(Component c) {
420: if (c instanceof AbstractButton) {
421: ((AbstractButton) c).addActionListener(this );
422: }
423: }
424:
425: public void unregister(Component c) {
426: if (c instanceof AbstractButton) {
427: ((AbstractButton) c).removeActionListener(this );
428: }
429: }
430: }
431:
432: /**
433: * This listener listens to menubar events. %%%
434: * The GUI needs to be redesigned then the implementation of this
435: * listener could be nicer, but in the meantime.
436: */
437: private class AIMenuBarListener extends AIContainerListener
438: implements ItemListener {
439:
440: private ProofAssistantController ctrl = ProofAssistantController.this ;
441:
442: public AIMenuBarListener(Container container) {
443: super (container);
444: }
445:
446: public void itemStateChanged(ItemEvent e) {
447: if (e.getStateChange() == ItemEvent.SELECTED) {
448: ctrl.assistantAI.analyze(
449: new PressedButtonEventInput((AbstractButton) e
450: .getSource(), AIInput.MENUBAR_EVENT))
451: .execute(ctrl);
452: }
453: }
454:
455: public void register(Component c) {
456: if (c instanceof AbstractButton) {
457: ((AbstractButton) c).addItemListener(this );
458: }
459: }
460:
461: public void unregister(Component c) {
462: if (c instanceof AbstractButton) {
463: ((AbstractButton) c).removeItemListener(this );
464: }
465: }
466: }
467:
468: /**
469: * This listener reacts on proof events
470: */
471: private class AIProofListener implements RuleAppListener,
472: AutoModeListener {
473:
474: private ProofAssistantController ctrl = ProofAssistantController.this ;
475: private boolean attentive = true;
476:
477: /**
478: * invoked if automatic execution has started
479: */
480: public void autoModeStarted(ProofEvent e) {
481: new Thread(unregisterCtrl).start();
482: attentive = false;
483: }
484:
485: /**
486: * invoked if automatic execution has stopped
487: */
488: public void autoModeStopped(ProofEvent e) {
489: new Thread(registerCtrl).start();
490: attentive = true;
491: }
492:
493: /**
494: * invoked when a rule has been applied
495: */
496: public void ruleApplied(ProofEvent e) {
497: if (enabled && attentive) {
498: if (e.getRuleAppInfo() != null) {
499: RuleApp appliedRule = e.getRuleAppInfo()
500: .getRuleApp();
501: ctrl.assistantAI.analyze(
502: new RuleEventInput(appliedRule)).execute(
503: ctrl);
504: }
505: }
506: }
507: }
508:
509: private class AIKeYSelectionListener implements
510: KeYSelectionListener {
511:
512: /** focused node has changed */
513: public void selectedNodeChanged(KeYSelectionEvent e) {
514: }
515:
516: /**
517: * the selected proof has changed
518: * (e.g. a new proof has been loaded)
519: */
520: public void selectedProofChanged(KeYSelectionEvent e) {
521: if (enabled) {
522: if (registered) {
523: new Thread(unregisterCtrl).start();
524: }
525: new Thread(registerCtrl).start();
526: }
527: }
528: }
529:
530: private class AISettingsListener implements SettingsListener {
531:
532: /**
533: * called by the Settings object to inform the listener that its
534: * state has changed
535: * @param e the Event sent to the listener
536: */
537: public void settingsChanged(GUIEvent e) {
538: if (e.getSource() instanceof GeneralSettings) {
539: GeneralSettings gSet = (GeneralSettings) e.getSource();
540: if (gSet.proofAssistantMode() != ProofAssistantController.this.enabled) {
541: if (enabled) {
542: ProofAssistantController.this.disable();
543: } else {
544: ProofAssistantController.this.enable();
545: }
546: }
547: }
548: }
549: }
550:
551: }
|