Source code: org/gjt/sp/jedit/help/HelpViewer.java
1 /*
2 * HelpViewer.java - HTML Help viewer
3 * :tabSize=8:indentSize=8:noTabs=false:
4 * :folding=explicit:collapseFolds=1:
5 *
6 * Copyright (C) 1999, 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.help;
24
25 //{{{ Imports
26 import javax.swing.*;
27 import javax.swing.border.*;
28 import javax.swing.event.*;
29 import javax.swing.text.html.*;
30 import java.awt.*;
31 import java.awt.event.*;
32 import java.beans.*;
33 import java.io.*;
34 import java.net.*;
35 import org.gjt.sp.jedit.gui.RolloverButton;
36 import org.gjt.sp.jedit.msg.PluginUpdate;
37 import org.gjt.sp.jedit.*;
38 import org.gjt.sp.util.Log;
39 //}}}
40
41 /**
42 * jEdit's searchable help viewer. It uses a Swing JEditorPane to display the HTML,
43 * and implements a URL history.
44 * @author Slava Pestov
45 * @version $Id: HelpViewer.java,v 1.12 2003/06/03 20:35:53 spestov Exp $
46 */
47 public class HelpViewer extends JFrame implements EBComponent
48 {
49 //{{{ HelpViewer constructor
50 /**
51 * Creates a new help viewer with the default help page.
52 * @since jEdit 4.0pre4
53 */
54 public HelpViewer()
55 {
56 this("welcome.html");
57 } //}}}
58
59 //{{{ HelpViewer constructor
60 /**
61 * Creates a new help viewer for the specified URL.
62 * @param url The URL
63 */
64 public HelpViewer(URL url)
65 {
66 this(url.toString());
67 } //}}}
68
69 //{{{ HelpViewer constructor
70 /**
71 * Creates a new help viewer for the specified URL.
72 * @param url The URL
73 */
74 public HelpViewer(String url)
75 {
76 super(jEdit.getProperty("helpviewer.title"));
77
78 setIconImage(GUIUtilities.getEditorIcon());
79
80 try
81 {
82 baseURL = new File(MiscUtilities.constructPath(
83 jEdit.getJEditHome(),"doc")).toURL().toString();
84 }
85 catch(MalformedURLException mu)
86 {
87 Log.log(Log.ERROR,this,mu);
88 // what to do?
89 }
90
91 history = new String[25];
92
93 ActionHandler actionListener = new ActionHandler();
94
95 JTabbedPane tabs = new JTabbedPane();
96 tabs.addTab(jEdit.getProperty("helpviewer.toc.label"),
97 toc = new HelpTOCPanel(this));
98 tabs.addTab(jEdit.getProperty("helpviewer.search.label"),
99 new HelpSearchPanel(this));
100 tabs.setMinimumSize(new Dimension(0,0));
101
102 JPanel rightPanel = new JPanel(new BorderLayout());
103
104 JToolBar toolBar = new JToolBar();
105 toolBar.setFloatable(false);
106
107 toolBar.add(title = new JLabel());
108 toolBar.add(Box.createGlue());
109
110 JPanel buttons = new JPanel();
111 buttons.setLayout(new BoxLayout(buttons,BoxLayout.X_AXIS));
112 buttons.setBorder(new EmptyBorder(0,12,0,0));
113 back = new RolloverButton(GUIUtilities.loadIcon(
114 jEdit.getProperty("helpviewer.back.icon")));
115 back.setToolTipText(jEdit.getProperty("helpviewer.back.label"));
116 back.addActionListener(actionListener);
117 toolBar.add(back);
118 forward = new RolloverButton(GUIUtilities.loadIcon(
119 jEdit.getProperty("helpviewer.forward.icon")));
120 forward.addActionListener(actionListener);
121 forward.setToolTipText(jEdit.getProperty("helpviewer.forward.label"));
122 toolBar.add(forward);
123 back.setPreferredSize(forward.getPreferredSize());
124
125 rightPanel.add(BorderLayout.NORTH,toolBar);
126
127 viewer = new JEditorPane();
128 viewer.setEditable(false);
129 viewer.addHyperlinkListener(new LinkHandler());
130 viewer.setFont(new Font("Monospaced",Font.PLAIN,12));
131 viewer.addPropertyChangeListener(new PropertyChangeHandler());
132
133 rightPanel.add(BorderLayout.CENTER,new JScrollPane(viewer));
134
135 splitter = new JSplitPane(JSplitPane.HORIZONTAL_SPLIT,
136 tabs,rightPanel);
137 splitter.setBorder(null);
138
139 getContentPane().add(BorderLayout.CENTER,splitter);
140
141 gotoURL(url,true);
142
143 setDefaultCloseOperation(DISPOSE_ON_CLOSE);
144
145 getRootPane().setPreferredSize(new Dimension(750,500));
146
147 pack();
148 GUIUtilities.loadGeometry(this,"helpviewer");
149
150 EditBus.addToBus(this);
151
152 show();
153
154 SwingUtilities.invokeLater(new Runnable()
155 {
156 public void run()
157 {
158 splitter.setDividerLocation(jEdit.getIntegerProperty(
159 "helpviewer.splitter",250));
160 viewer.requestFocus();
161 }
162 });
163 } //}}}
164
165 //{{{ gotoURL() method
166 /**
167 * Displays the specified URL in the HTML component.
168 * @param url The URL
169 * @param addToHistory Should the URL be added to the back/forward
170 * history?
171 */
172 public void gotoURL(String url, boolean addToHistory)
173 {
174 // the TOC pane looks up user's guide URLs relative to the
175 // doc directory...
176 String shortURL;
177 if(MiscUtilities.isURL(url))
178 {
179 if(url.startsWith(baseURL))
180 {
181 shortURL = url.substring(baseURL.length());
182 if(shortURL.startsWith("/"))
183 shortURL = shortURL.substring(1);
184 }
185 else
186 {
187 shortURL = url;
188 }
189 }
190 else
191 {
192 shortURL = url;
193 if(baseURL.endsWith("/"))
194 url = baseURL + url;
195 else
196 url = baseURL + '/' + url;
197 }
198
199 // reset default cursor so that the hand cursor doesn't
200 // stick around
201 viewer.setCursor(Cursor.getDefaultCursor());
202
203 URL _url = null;
204 try
205 {
206 _url = new URL(url);
207
208 if(!_url.equals(viewer.getPage()))
209 title.setText(jEdit.getProperty("helpviewer.loading"));
210 else
211 {
212 /* don't show loading msg because we won't
213 receive a propertyChanged */
214 }
215
216 viewer.setPage(_url);
217 if(addToHistory)
218 {
219 history[historyPos] = url;
220 if(historyPos + 1 == history.length)
221 {
222 System.arraycopy(history,1,history,
223 0,history.length - 1);
224 history[historyPos] = null;
225 }
226 else
227 historyPos++;
228 }
229 }
230 catch(MalformedURLException mf)
231 {
232 Log.log(Log.ERROR,this,mf);
233 String[] args = { url, mf.getMessage() };
234 GUIUtilities.error(this,"badurl",args);
235 return;
236 }
237 catch(IOException io)
238 {
239 Log.log(Log.ERROR,this,io);
240 String[] args = { url, io.toString() };
241 GUIUtilities.error(this,"read-error",args);
242 return;
243 }
244
245 this.shortURL = shortURL;
246
247 // select the appropriate tree node.
248 if(shortURL != null)
249 toc.selectNode(shortURL);
250 } //}}}
251
252 //{{{ dispose() method
253 public void dispose()
254 {
255 EditBus.removeFromBus(this);
256 jEdit.setIntegerProperty("helpviewer.splitter",
257 splitter.getDividerLocation());
258 GUIUtilities.saveGeometry(this,"helpviewer");
259 super.dispose();
260 } //}}}
261
262 //{{{ handleMessage() method
263 public void handleMessage(EBMessage msg)
264 {
265 if(msg instanceof PluginUpdate)
266 {
267 PluginUpdate pmsg = (PluginUpdate)msg;
268 if(pmsg.getWhat() == PluginUpdate.LOADED
269 || pmsg.getWhat() == PluginUpdate.UNLOADED)
270 {
271 if(pmsg.isExiting())
272 {
273 // we don't care
274 }
275
276 if(!queuedTOCReload)
277 queueTOCReload();
278 queuedTOCReload = true;
279 }
280 }
281 } //}}}
282
283 //{{{ getBaseURL() method
284 public String getBaseURL()
285 {
286 return baseURL;
287 } //}}}
288
289 //{{{ getShortURL() method
290 String getShortURL()
291 {
292 return shortURL;
293 } //}}}
294
295 //{{{ Private members
296
297 //{{{ Instance members
298 private String baseURL;
299 private String shortURL;
300 private JButton back;
301 private JButton forward;
302 private JEditorPane viewer;
303 private JLabel title;
304 private JSplitPane splitter;
305 private String[] history;
306 private int historyPos;
307 private HelpTOCPanel toc;
308 private boolean queuedTOCReload;
309 //}}}
310
311 //{{{ queueTOCReload() method
312 public void queueTOCReload()
313 {
314 SwingUtilities.invokeLater(new Runnable()
315 {
316 public void run()
317 {
318 queuedTOCReload = false;
319 toc.load();
320 }
321 });
322 } //}}}
323
324 //}}}
325
326 //{{{ Inner classes
327
328 //{{{ ActionHandler class
329 class ActionHandler implements ActionListener
330 {
331 //{{{ actionPerformed() class
332 public void actionPerformed(ActionEvent evt)
333 {
334 Object source = evt.getSource();
335 if(source == back)
336 {
337 if(historyPos <= 1)
338 getToolkit().beep();
339 else
340 {
341 String url = history[--historyPos - 1];
342 gotoURL(url,false);
343 }
344 }
345 else if(source == forward)
346 {
347 if(history.length - historyPos <= 1)
348 getToolkit().beep();
349 else
350 {
351 String url = history[historyPos];
352 if(url == null)
353 getToolkit().beep();
354 else
355 {
356 historyPos++;
357 gotoURL(url,false);
358 }
359 }
360 }
361 } //}}}
362 } //}}}
363
364 //{{{ LinkHandler class
365 class LinkHandler implements HyperlinkListener
366 {
367 //{{{ hyperlinkUpdate() method
368 public void hyperlinkUpdate(HyperlinkEvent evt)
369 {
370 if(evt.getEventType() == HyperlinkEvent.EventType.ACTIVATED)
371 {
372 if(evt instanceof HTMLFrameHyperlinkEvent)
373 {
374 ((HTMLDocument)viewer.getDocument())
375 .processHTMLFrameHyperlinkEvent(
376 (HTMLFrameHyperlinkEvent)evt);
377 }
378 else
379 {
380 URL url = evt.getURL();
381 if(url != null)
382 gotoURL(url.toString(),true);
383 }
384 }
385 else if (evt.getEventType() == HyperlinkEvent.EventType.ENTERED) {
386 viewer.setCursor(Cursor.getPredefinedCursor(Cursor.HAND_CURSOR));
387 }
388 else if (evt.getEventType() == HyperlinkEvent.EventType.EXITED) {
389 viewer.setCursor(Cursor.getDefaultCursor());
390 }
391 } //}}}
392 } //}}}
393
394 //{{{ PropertyChangeHandler class
395 class PropertyChangeHandler implements PropertyChangeListener
396 {
397 public void propertyChange(PropertyChangeEvent evt)
398 {
399 if("page".equals(evt.getPropertyName()))
400 {
401 String titleStr = (String)viewer.getDocument()
402 .getProperty("title");
403 if(titleStr == null)
404 {
405 titleStr = MiscUtilities.getFileName(
406 viewer.getPage().toString());
407 }
408 title.setText(titleStr);
409 }
410 }
411 } //}}}
412
413 //}}}
414 }