Source code: org/gjt/sp/jedit/gui/TipOfTheDay.java
1 /*
2 * TipOfTheDay.java - Tip of the day window
3 * :tabSize=8:indentSize=8:noTabs=false:
4 * :folding=explicit:collapseFolds=1:
5 *
6 * Copyright (C) 2000, 2001, 2002 Slava Pestov
7 *
8 * This program is free software; you can redistribute it and/or
9 * modify it under the terms of the GNU General Public License
10 * as published by the Free Software Foundation; either version 2
11 * of the License, or any later version.
12 *
13 * This program is distributed in the hope that it will be useful,
14 * but WITHOUT ANY WARRANTY; without even the implied warranty of
15 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
16 * GNU General Public License for more details.
17 *
18 * You should have received a copy of the GNU General Public License
19 * along with this program; if not, write to the Free Software
20 * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
21 */
22
23 package org.gjt.sp.jedit.gui;
24
25 //{{{ Imports
26 import javax.swing.border.EmptyBorder;
27 import javax.swing.*;
28 import java.awt.event.*;
29 import java.awt.*;
30 import java.io.*;
31 import java.util.Random;
32 import org.gjt.sp.jedit.*;
33 import org.gjt.sp.util.Log;
34 //}}}
35
36 public class TipOfTheDay extends EnhancedDialog
37 {
38 //{{{ TipOfTheDay constructor
39 public TipOfTheDay(View view)
40 {
41 super(view,jEdit.getProperty("tip.title"),false);
42
43 JPanel content = new JPanel(new BorderLayout(12,12));
44 content.setBorder(new EmptyBorder(12,12,12,12));
45 setContentPane(content);
46
47 JLabel label = new JLabel(jEdit.getProperty("tip.caption"));
48 label.setFont(new Font("SansSerif",Font.PLAIN,24));
49 label.setForeground(UIManager.getColor("Button.foreground"));
50 content.add(BorderLayout.NORTH,label);
51
52 tipText = new JEditorPane();
53 tipText.setEditable(false);
54 tipText.setContentType("text/html");
55
56 nextTip();
57
58 JScrollPane scroller = new JScrollPane(tipText);
59 scroller.setPreferredSize(new Dimension(150,150));
60 content.add(BorderLayout.CENTER,scroller);
61
62 ActionHandler actionHandler = new ActionHandler();
63
64 Box buttons = new Box(BoxLayout.X_AXIS);
65
66 showNextTime = new JCheckBox(jEdit.getProperty("tip.show-next-time"),
67 jEdit.getBooleanProperty("tip.show"));
68 showNextTime.addActionListener(actionHandler);
69 buttons.add(showNextTime);
70
71 buttons.add(Box.createHorizontalStrut(6));
72 buttons.add(Box.createGlue());
73
74 nextTip = new JButton(jEdit.getProperty("tip.next-tip"));
75 nextTip.addActionListener(actionHandler);
76 buttons.add(nextTip);
77
78 buttons.add(Box.createHorizontalStrut(6));
79
80 close = new JButton(jEdit.getProperty("common.close"));
81 close.addActionListener(actionHandler);
82 buttons.add(close);
83 content.getRootPane().setDefaultButton(close);
84
85 Dimension dim = nextTip.getPreferredSize();
86 dim.width = Math.max(dim.width,close.getPreferredSize().width);
87 nextTip.setPreferredSize(dim);
88 close.setPreferredSize(dim);
89
90 content.add(BorderLayout.SOUTH,buttons);
91
92 setDefaultCloseOperation(DISPOSE_ON_CLOSE);
93 pack();
94 setLocationRelativeTo(view);
95 show();
96 } //}}}
97
98 //{{{ ok() method
99 public void ok()
100 {
101 dispose();
102 } //}}}
103
104 //{{{ cancel() method
105 public void cancel()
106 {
107 dispose();
108 } //}}}
109
110 //{{{ Private members
111
112 //{{{ Instance variables
113 private JCheckBox showNextTime;
114 private JButton nextTip, close;
115 private JEditorPane tipText;
116 private int currentTip = -1;
117 //}}}
118
119 //{{{ nextTip() method
120 private void nextTip()
121 {
122 File[] tips = new File(MiscUtilities.constructPath(
123 jEdit.getJEditHome(),"doc","tips")).listFiles();
124 if(tips == null || tips.length == 0)
125 {
126 tipText.setText(jEdit.getProperty("tip.not-found"));
127 return;
128 }
129
130 int count = tips.length;
131
132 // so that we don't see the same tip again if the user
133 // clicks 'Next Tip'
134 int tipToShow = currentTip;
135 while(tipToShow == currentTip || !tips[tipToShow].getName().endsWith(".html"))
136 tipToShow = Math.abs(new Random().nextInt()) % count;
137 try
138 {
139 tipText.setPage(tips[tipToShow].toURL());
140 }
141 catch(Exception e)
142 {
143 Log.log(Log.ERROR,this,e);
144 }
145 } //}}}
146
147 //}}}
148
149 //{{{ ActionHandler class
150 class ActionHandler implements ActionListener
151 {
152 public void actionPerformed(ActionEvent evt)
153 {
154 Object source = evt.getSource();
155 if(source == showNextTime)
156 {
157 jEdit.setBooleanProperty("tip.show",showNextTime
158 .isSelected());
159 }
160 else if(source == nextTip)
161 nextTip();
162 else if(source == close)
163 dispose();
164 }
165 } //}}}
166 }