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:
011: /** common superclass of TacletIfSelectionDialog and TacletMatchCompletionDialog */package de.uka.ilkd.key.gui;
012:
013: import java.awt.*;
014: import java.awt.event.ActionListener;
015: import java.awt.event.WindowAdapter;
016: import java.awt.event.WindowEvent;
017: import java.io.StringWriter;
018: import java.io.Writer;
019:
020: import javax.swing.*;
021: import javax.swing.border.TitledBorder;
022:
023: import org.apache.log4j.Logger;
024:
025: import de.uka.ilkd.key.gui.configuration.ProofSettings;
026: import de.uka.ilkd.key.logic.ListOfNamed;
027: import de.uka.ilkd.key.pp.LogicPrinter;
028: import de.uka.ilkd.key.pp.ProgramPrinter;
029: import de.uka.ilkd.key.proof.ApplyTacletDialogModel;
030: import de.uka.ilkd.key.rule.Taclet;
031: import de.uka.ilkd.key.rule.inst.SVInstantiations;
032: import de.uka.ilkd.key.util.pp.StringBackend;
033:
034: public abstract class ApplyTacletDialog extends JDialog {
035:
036: // buttons
037: protected JButton cancelButton;
038: protected JButton applyButton;
039:
040: private KeYMediator mediator;
041: protected boolean checkAfterEachInput = true;
042:
043: protected ApplyTacletDialogModel[] model;
044: private JTextArea statusArea;
045: private JPanel statusPanel;
046:
047: public ApplyTacletDialog(ApplyTacletDialogModel[] model,
048: KeYMediator mediator) {
049:
050: super (mediator.mainFrame(), "Choose Taclet Instantiation",
051: false);
052: // setSize(800,700);
053: // setLocation(70,50);
054:
055: this .mediator = mediator;
056: this .model = model;
057:
058: applyButton = new JButton("Apply");
059: cancelButton = new JButton("Cancel");
060:
061: mediator.requestModalAccess(this );
062: addWindowListener(new WindowAdapter() {
063: public void windowClosed(WindowEvent e) {
064: ApplyTacletDialog.this .closeDlg();
065: }
066:
067: public void windowClosing(WindowEvent e) {
068: ApplyTacletDialog.this .closeDlg();
069: }
070: });
071: }
072:
073: protected KeYMediator mediator() {
074: return mediator;
075: }
076:
077: private int countLines(String s) {
078: int i = 0;
079: int p = 0;
080: while ((p = s.indexOf("\n", p)) >= 0) {
081: i++;
082: p++;
083: }
084: return i + 1;
085: }
086:
087: protected JPanel createInfoPanel() {
088: ListOfNamed vars = model[0].programVariables().elements();
089: JPanel panel = new JPanel(new GridLayout(1, 1));
090: panel.setBorder(new TitledBorder("Sequent program variables"));
091: JScrollPane scroll = new JScrollPane();
092: JTextArea text;
093: if (vars.size() > 0) {
094: text = new JTextArea(vars.toString(), 2, 40);
095: } else {
096: text = new JTextArea("none", 1, 40);
097: }
098: scroll.setViewportView(text);
099: text.setEditable(false);
100: panel.add(scroll, BorderLayout.CENTER);
101: return panel;
102: }
103:
104: protected JPanel createTacletDisplay() {
105: JPanel panel = new JPanel(new BorderLayout());
106: panel.setBorder(new TitledBorder("Selected Taclet - "
107: + model[0].taclet().name()));
108: if (logger.isDebugEnabled()) {
109: logger.debug("TacletApp: " + model[0].taclet());
110: }
111: Taclet taclet = model[0].taclet();
112: StringBackend backend = new StringBackend(68);
113: StringBuffer tacletSB = new StringBuffer();
114:
115: Writer w = new StringWriter();
116: //WriterBackend backend = new WriterBackend(w, 68);
117:
118: LogicPrinter tp = new LogicPrinter(new ProgramPrinter(w),
119: de.uka.ilkd.key.pp.NotationInfo.createInstance(),
120: backend, mediator.getServices(), true);
121:
122: // tp.printTaclet(taclet, model[0].tacletApp().instantiations(),
123: tp.printTaclet(taclet, SVInstantiations.EMPTY_SVINSTANTIATIONS,
124: ProofSettings.DEFAULT_SETTINGS.getViewSettings()
125: .getShowWholeTaclet());
126: tacletSB.append(backend.getString());
127:
128: //logger.info(tacletSB);
129: //System.out.println(tacletSB);
130:
131: panel.setAlignmentY(JPanel.TOP_ALIGNMENT);
132: // show taclet
133: JScrollPane scroll = new JScrollPane();
134: int nolines = countLines(model[0].taclet().toString()) + 1;
135: if (nolines > 10)
136: nolines = 11;
137: //JTextArea text=new JTextArea(model[0].taclet().toString(),nolines,40);
138: JTextArea text = new JTextArea(tacletSB.toString(), nolines, 68);
139: text.setEditable(false);
140: scroll.setViewportView(text);
141: panel.add(scroll, BorderLayout.CENTER);
142:
143: return panel;
144: }
145:
146: protected abstract void pushAllInputToModel();
147:
148: protected abstract int current();
149:
150: public boolean checkAfterEachInput() {
151: return checkAfterEachInput;
152: }
153:
154: protected JPanel createStatusPanel() {
155: statusPanel = new JPanel(new BorderLayout());
156:
157: statusArea = new JTextArea();
158: statusArea.setEditable(false);
159:
160: statusPanel.add(new JScrollPane(statusArea,
161: JScrollPane.VERTICAL_SCROLLBAR_AS_NEEDED,
162: JScrollPane.HORIZONTAL_SCROLLBAR_AS_NEEDED),
163: BorderLayout.CENTER);
164: statusPanel.setBorder(new TitledBorder(
165: "Input validation result"));
166: setStatus(model[current()].getStatusString());
167: return statusPanel;
168: }
169:
170: protected JPanel createButtonPanel(ActionListener buttonListener) {
171: JPanel panel = new JPanel(new GridBagLayout());
172: GridBagConstraints c = new GridBagConstraints();
173:
174: cancelButton.addActionListener(buttonListener);
175: applyButton.addActionListener(buttonListener);
176: c.insets = new Insets(5, 20, 5, 20);
177: c.gridx = 0;
178: panel.add(cancelButton, c);
179:
180: c.gridx = 1;
181: panel.add(applyButton, c);
182: panel.setAlignmentY(JPanel.BOTTOM_ALIGNMENT);
183:
184: return panel;
185: }
186:
187: protected void setStatus(String s) {
188: if (statusArea != null) {
189: statusArea.setText(s);
190: }
191: }
192:
193: protected void closeDlg() {
194: mediator.freeModalAccess(this );
195: }
196:
197: static Logger logger = Logger.getLogger(ApplyTacletDialog.class
198: .getName());
199: }
|