01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09: // This file is part of KeY - Integrated Deductive Software Design
10: // Copyright (C) 2001-2004 Universitaet Karlsruhe, Germany
11: // Universitaet Koblenz-Landau, Germany
12: // Chalmers University of Technology, Sweden
13: //
14: // The KeY system is protected by the GNU General Public License.
15: // See LICENSE.TXT for details.
16: package de.uka.ilkd.key.gui.assistant;
17:
18: import de.uka.ilkd.key.rule.Rule;
19: import de.uka.ilkd.key.rule.RuleApp;
20:
21: /**
22: * A rule event has happend. The corresponding rule application object
23: * is encapsulated by the input object and can be evaluated by the
24: * proof assistant AI.
25: */
26: public class RuleEventInput implements AIInput {
27:
28: /** the rule application to be evaluated */
29: private final RuleApp ruleApp;
30:
31: public RuleEventInput(RuleApp app) {
32: this .ruleApp = app;
33: }
34:
35: /** returns the rule application */
36: public RuleApp getRuleApp() {
37: return ruleApp;
38: }
39:
40: /** return the rule */
41: public Rule getRule() {
42: return ruleApp.rule();
43: }
44:
45: /**
46: * returns the AI input identifier
47: */
48: public int getInputID() {
49: return RULE_APPLICATION_EVENT;
50: }
51:
52: /** toString */
53: public String toString() {
54: return "RuleEvent: " + getInputID()
55: + "\n for Rule Application:" + getRuleApp();
56: }
57:
58: }
|