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: //
10: package de.uka.ilkd.key.gui;
11:
12: import java.awt.*;
13: import java.awt.event.ActionEvent;
14: import java.awt.event.ActionListener;
15: import java.io.ByteArrayOutputStream;
16:
17: import javax.swing.*;
18:
19: public class ErrorMessages {
20:
21: private ErrorMessages() {
22: }
23:
24: public static void showBugMessage(Frame owner, String s, Exception e) {
25: showBugHelp(new JDialog(owner, "Internal error", true), s, e);
26: }
27:
28: public static void showBugMessage(Dialog owner, String s,
29: Exception e) {
30: showBugHelp(new JDialog(owner, "Internal error", true), s, e);
31: }
32:
33: private static void showBugHelp(JDialog f, String s, Exception e) {
34: JPanel p = new JPanel();
35: p.setLayout(new BorderLayout());
36: p.setBorder(new javax.swing.border.TitledBorder(""));
37: JPanel mp = new JPanel();
38: mp.setLayout(new BoxLayout(mp, BoxLayout.Y_AXIS));
39: mp.add(new JLabel(
40: "An internal error in the KeY system occurred."));
41: mp.add(new JLabel(">>" + s + "<<"));
42: mp.add(new JLabel());
43: mp.add(new JLabel("Please, report this error to the KeY team"));
44: mp.add(new JLabel(
45: "by describing what you did and by submitting"));
46: mp.add(new JLabel("the complete stack trace from below."));
47: mp
48: .add(new JLabel(
49: "If you have access, please use the KeY Bugtracker at"));
50: mp.add(new JLabel("http://i12www.ira.uka.de/~klebanov/mantis"));
51: p.add(mp, BorderLayout.NORTH);
52: ByteArrayOutputStream byteOut = new ByteArrayOutputStream();
53: java.io.PrintStream out = new java.io.PrintStream(byteOut);
54: e.printStackTrace(out);
55: JTextArea stack = new JTextArea(">>" + s + "<<\n"
56: + byteOut.toString(), 10, 30);
57: JScrollPane scroll = new JScrollPane();
58: scroll.setViewportView(stack);
59: stack.setEditable(false);
60: p.add(scroll, BorderLayout.CENTER);
61:
62: JPanel bp = new JPanel(new GridBagLayout());
63: GridBagConstraints c = new GridBagConstraints();
64:
65: ActionListener dlgCloseListener = new ActionListener() {
66: public void actionPerformed(ActionEvent ae) {
67: Component cm = (Component) ae.getSource();
68: while (!(cm instanceof Window)) {
69: cm = cm.getParent();
70: }
71: ((Window) cm).setVisible(false);
72: ((Window) cm).dispose();
73: }
74: };
75: JButton okb = new JButton("Done");
76: okb.addActionListener(dlgCloseListener);
77: c.insets = new Insets(5, 20, 5, 20);
78: c.gridx = 0;
79: bp.add(okb, c);
80: bp.setAlignmentY(JPanel.BOTTOM_ALIGNMENT);
81: p.add(bp, BorderLayout.SOUTH);
82: f.getContentPane().add(p);
83: f.pack();
84: f.setVisible(true);
85: }
86:
87: public static void handleExceptionType(Frame owner, String s,
88: Exception e) {
89: if (e instanceof NullPointerException
90: || e instanceof ClassCastException) {
91: showBugMessage(owner, s, e);
92: }
93: }
94:
95: }
|