001: /*
002: * TipOfTheDay.java - Tip of the day window
003: * :tabSize=8:indentSize=8:noTabs=false:
004: * :folding=explicit:collapseFolds=1:
005: *
006: * Copyright (C) 2000, 2001, 2002 Slava Pestov
007: *
008: * This program is free software; you can redistribute it and/or
009: * modify it under the terms of the GNU General Public License
010: * as published by the Free Software Foundation; either version 2
011: * of the License, or any later version.
012: *
013: * This program is distributed in the hope that it will be useful,
014: * but WITHOUT ANY WARRANTY; without even the implied warranty of
015: * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
016: * GNU General Public License for more details.
017: *
018: * You should have received a copy of the GNU General Public License
019: * along with this program; if not, write to the Free Software
020: * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
021: */
022:
023: package org.gjt.sp.jedit.gui;
024:
025: //{{{ Imports
026: import javax.swing.border.EmptyBorder;
027: import javax.swing.*;
028: import java.awt.event.*;
029: import java.awt.*;
030: import java.io.*;
031: import java.util.Random;
032: import org.gjt.sp.jedit.*;
033: import org.gjt.sp.util.Log;
034:
035: //}}}
036:
037: public class TipOfTheDay extends EnhancedDialog {
038: //{{{ TipOfTheDay constructor
039: public TipOfTheDay(View view) {
040: super (view, jEdit.getProperty("tip.title"), false);
041:
042: JPanel content = new JPanel(new BorderLayout(12, 12));
043: content.setBorder(new EmptyBorder(12, 12, 12, 12));
044: setContentPane(content);
045:
046: JLabel label = new JLabel(jEdit.getProperty("tip.caption"));
047: label.setFont(new Font("SansSerif", Font.PLAIN, 24));
048: label.setForeground(UIManager.getColor("Button.foreground"));
049: content.add(BorderLayout.NORTH, label);
050:
051: tipText = new JEditorPane();
052: tipText.setEditable(false);
053: tipText.setContentType("text/html");
054:
055: nextTip();
056:
057: JScrollPane scroller = new JScrollPane(tipText);
058: scroller.setPreferredSize(new Dimension(150, 150));
059: content.add(BorderLayout.CENTER, scroller);
060:
061: ActionHandler actionHandler = new ActionHandler();
062:
063: Box buttons = new Box(BoxLayout.X_AXIS);
064:
065: showNextTime = new JCheckBox(jEdit
066: .getProperty("tip.show-next-time"), jEdit
067: .getBooleanProperty("tip.show"));
068: showNextTime.addActionListener(actionHandler);
069: buttons.add(showNextTime);
070:
071: buttons.add(Box.createHorizontalStrut(6));
072: buttons.add(Box.createGlue());
073:
074: nextTip = new JButton(jEdit.getProperty("tip.next-tip"));
075: nextTip.addActionListener(actionHandler);
076: buttons.add(nextTip);
077:
078: buttons.add(Box.createHorizontalStrut(6));
079:
080: close = new JButton(jEdit.getProperty("common.close"));
081: close.addActionListener(actionHandler);
082: buttons.add(close);
083: content.getRootPane().setDefaultButton(close);
084:
085: Dimension dim = nextTip.getPreferredSize();
086: dim.width = Math.max(dim.width, close.getPreferredSize().width);
087: nextTip.setPreferredSize(dim);
088: close.setPreferredSize(dim);
089:
090: content.add(BorderLayout.SOUTH, buttons);
091:
092: setDefaultCloseOperation(DISPOSE_ON_CLOSE);
093: pack();
094: setLocationRelativeTo(view);
095: setVisible(true);
096: } //}}}
097:
098: //{{{ ok() method
099: public void ok() {
100: dispose();
101: } //}}}
102:
103: //{{{ cancel() method
104: public void cancel() {
105: dispose();
106: } //}}}
107:
108: //{{{ Private members
109:
110: //{{{ Instance variables
111: private JCheckBox showNextTime;
112: private JButton nextTip, close;
113: private JEditorPane tipText;
114: private int currentTip = -1;
115:
116: //}}}
117:
118: //{{{ nextTip() method
119: private void nextTip() {
120: File[] tips = new File(MiscUtilities.constructPath(jEdit
121: .getJEditHome(), "doc", "tips")).listFiles();
122: if (tips == null || tips.length == 0) {
123: tipText.setText(jEdit.getProperty("tip.not-found"));
124: return;
125: }
126:
127: int count = tips.length;
128:
129: // so that we don't see the same tip again if the user
130: // clicks 'Next Tip'
131: int tipToShow = currentTip;
132: while (tipToShow == currentTip
133: || !tips[tipToShow].getName().endsWith(".html"))
134: tipToShow = Math.abs(new Random().nextInt()) % count;
135: try {
136: tipText.setPage(tips[tipToShow].toURL());
137: } catch (Exception e) {
138: Log.log(Log.ERROR, this , e);
139: }
140: } //}}}
141:
142: //}}}
143:
144: //{{{ ActionHandler class
145: class ActionHandler implements ActionListener {
146: public void actionPerformed(ActionEvent evt) {
147: Object source = evt.getSource();
148: if (source == showNextTime) {
149: jEdit.setBooleanProperty("tip.show", showNextTime
150: .isSelected());
151: } else if (source == nextTip)
152: nextTip();
153: else if (source == close)
154: dispose();
155: }
156: } //}}}
157: }
|