001: /*BEGIN_COPYRIGHT_BLOCK
002: *
003: * Copyright (c) 2001-2007, JavaPLT group at Rice University (javaplt@rice.edu)
004: * All rights reserved.
005: *
006: * Redistribution and use in source and binary forms, with or without
007: * modification, are permitted provided that the following conditions are met:
008: * * Redistributions of source code must retain the above copyright
009: * notice, this list of conditions and the following disclaimer.
010: * * Redistributions in binary form must reproduce the above copyright
011: * notice, this list of conditions and the following disclaimer in the
012: * documentation and/or other materials provided with the distribution.
013: * * Neither the names of DrJava, the JavaPLT group, Rice University, nor the
014: * names of its contributors may be used to endorse or promote products
015: * derived from this software without specific prior written permission.
016: *
017: * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
018: * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
019: * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
020: * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR
021: * CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
022: * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
023: * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
024: * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
025: * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
026: * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
027: * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
028: *
029: * This software is Open Source Initiative approved Open Source Software.
030: * Open Source Initative Approved is a trademark of the Open Source Initiative.
031: *
032: * This file is part of DrJava. Download the current version of this project
033: * from http://www.drjava.org/ or http://sourceforge.net/projects/drjava/
034: *
035: * END_COPYRIGHT_BLOCK*/
036:
037: package edu.rice.cs.drjava.ui;
038:
039: import javax.swing.*;
040: import javax.swing.event.*;
041: import javax.swing.border.*;
042: import javax.swing.text.html.*;
043: import java.awt.event.*;
044: import java.awt.*;
045: import java.net.*;
046: import java.io.*;
047: import java.util.Vector;
048:
049: import edu.rice.cs.util.FileOps;
050: import edu.rice.cs.util.UnexpectedException;
051: import edu.rice.cs.util.swing.BorderlessScrollPane;
052:
053: /** The frame for displaying the HTML help files.
054: * @version $Id: HTMLFrame.java 4255 2007-08-28 19:17:37Z mgricken $
055: */
056: public class HTMLFrame extends JFrame {
057:
058: private static final int FRAME_WIDTH = 750;
059: private static final int FRAME_HEIGHT = 600;
060: private static final int LEFT_PANEL_WIDTH = 250;
061: private JEditorPane _mainDocPane;
062: private JScrollPane _mainScroll;
063: private JSplitPane _splitPane;
064: private JPanel _splitPaneHolder;
065: private JEditorPane _contentsDocPane;
066: private JPanel _closePanel;
067: private JButton _closeButton;
068: private JButton _backButton;
069: private JButton _forwardButton;
070: protected URL _baseURL;
071: private Vector<HyperlinkListener> _hyperlinkListeners;
072: private boolean _linkError;
073: private URL _lastURL;
074:
075: private JPanel _navPane;
076:
077: protected HistoryList _history;
078:
079: private HyperlinkListener _resetListener = new HyperlinkListener() {
080: public void hyperlinkUpdate(HyperlinkEvent e) {
081: if (_linkError
082: && e.getEventType() == HyperlinkEvent.EventType.ACTIVATED) {
083: _resetMainPane();
084: }
085: }
086: };
087:
088: protected static class HistoryList {
089: private HistoryList next = null;
090: private final HistoryList prev;
091: protected final URL contents;
092:
093: private HistoryList(URL contents) {
094: this .contents = contents;
095: this .prev = null;
096: }
097:
098: private HistoryList(URL contents, HistoryList prev) {
099: this .contents = contents;
100: this .prev = prev;
101: prev.next = this ;
102: }
103: }
104:
105: public static abstract class ResourceAction extends AbstractAction {
106: public ResourceAction(String name, String iconName) {
107: super (name, MainFrame.getIcon(iconName));
108: }
109: }
110:
111: private static abstract class ConsolidatedAction extends
112: ResourceAction {
113: private ConsolidatedAction(String name) {
114: super (name, name + "16.gif");
115: }
116: }
117:
118: private Action _forwardAction = new ConsolidatedAction("Forward") {
119: public void actionPerformed(ActionEvent e) {
120: _history = _history.next;
121:
122: // user is always allowed to move back after a forward.
123: _backAction.setEnabled(true);
124:
125: if (_history.next == null) {
126: // no more forwards after this
127: _forwardAction.setEnabled(false);
128: }
129: _displayPage(_history.contents);
130: }
131: };
132:
133: private Action _backAction = new ConsolidatedAction("Back") {
134: public void actionPerformed(ActionEvent e) {
135: _history = _history.prev;
136:
137: // user is always allowed to move forward after backing up
138: _forwardAction.setEnabled(true);
139:
140: if (_history.prev == null) {
141: // no more backing up
142: _backAction.setEnabled(false);
143: }
144: _displayPage(_history.contents);
145: }
146: };
147:
148: private Action _closeAction = new AbstractAction("Close") {
149: public void actionPerformed(ActionEvent e) {
150: HTMLFrame.this .setVisible(false);
151: }
152: };
153:
154: private static JButton makeButton(Action a, int horTextPos,
155: int left, int right) {
156: JButton j = new JButton(a);
157: j.setHorizontalTextPosition(horTextPos);
158: j.setVerticalTextPosition(JButton.CENTER);
159: //Insets i = j.getMargin();
160: //j.setMargin(new Insets(i.top,left,i.bottom,right));
161: j.setMargin(new Insets(3, left + 3, 3, right + 3));
162: return j;
163: }
164:
165: public void addHyperlinkListener(HyperlinkListener linkListener) {
166: _hyperlinkListeners.add(linkListener);
167: _contentsDocPane.addHyperlinkListener(linkListener);
168: _mainDocPane.addHyperlinkListener(linkListener);
169: }
170:
171: /**
172: * Sets up the frame and displays it.
173: */
174: public HTMLFrame(String frameName, URL introUrl, URL indexUrl,
175: String iconString) {
176: this (frameName, introUrl, indexUrl, iconString, null);
177: }
178:
179: /**
180: * Sets up the frame and displays it.
181: */
182: public HTMLFrame(String frameName, URL introUrl, URL indexUrl,
183: String iconString, File baseDir) {
184: super (frameName);
185:
186: _contentsDocPane = new JEditorPane();
187: _contentsDocPane.setEditable(false);
188: JScrollPane contentsScroll = new BorderlessScrollPane(
189: _contentsDocPane);
190:
191: _mainDocPane = new JEditorPane();
192: _mainDocPane.setEditable(false);
193: _mainScroll = new BorderlessScrollPane(_mainDocPane);
194:
195: _splitPane = new JSplitPane(JSplitPane.HORIZONTAL_SPLIT, true,
196: contentsScroll, _mainScroll);
197: _splitPane.setDividerLocation(LEFT_PANEL_WIDTH);
198: _splitPaneHolder = new JPanel(new GridLayout(1, 1));
199: _splitPaneHolder.setBorder(new EmptyBorder(0, 5, 0, 5));
200: _splitPaneHolder.add(_splitPane);
201: // _splitPane.setBorder(new CompoundBorder(new EmptyBorder(0,5,0,5),_splitPane.getBorder()));
202: _closeButton = new JButton(_closeAction);
203: _backButton = makeButton(_backAction, JButton.RIGHT, 0, 3);
204: _forwardButton = makeButton(_forwardAction, JButton.LEFT, 3, 0);
205: _backAction.setEnabled(false);
206: _forwardAction.setEnabled(false);
207: _closePanel = new JPanel(new BorderLayout());
208: _closePanel.add(_closeButton, BorderLayout.EAST);
209: _closePanel.setBorder(new EmptyBorder(5, 5, 5, 5)); // padding
210: _navPane = new JPanel();
211: _navPane.setBackground(new Color(0xCCCCFF));
212: _navPane.setLayout(new BoxLayout(_navPane, BoxLayout.X_AXIS));
213: JLabel icon = new JLabel(MainFrame.getIcon(iconString));
214: _navPane.add(icon);
215: _navPane.add(Box.createHorizontalStrut(8));
216: _navPane.add(Box.createHorizontalGlue());
217: _navPane.add(_backButton);
218: _navPane.add(Box.createHorizontalStrut(8));
219: _navPane.add(_forwardButton);
220: _navPane.add(Box.createHorizontalStrut(3));
221: _navPane.setBorder(new EmptyBorder(0, 0, 0, 5));
222: JPanel navContainer = new JPanel(new GridLayout(1, 1));
223: navContainer.setBorder(new CompoundBorder(new EmptyBorder(5, 5,
224: 5, 5), new EtchedBorder()));
225: //new BevelBorder(BevelBorder.LOWERED)));
226: navContainer.add(_navPane);
227: Container cp = getContentPane();
228: cp.setLayout(new BorderLayout());
229: cp.add(navContainer, BorderLayout.NORTH);
230: cp.add(_splitPaneHolder, BorderLayout.CENTER);
231: cp.add(_closePanel, BorderLayout.SOUTH);
232:
233: _linkError = false;
234: _hyperlinkListeners = new Vector<HyperlinkListener>();
235: _hyperlinkListeners.add(_resetListener);
236: _mainDocPane.addHyperlinkListener(_resetListener);
237:
238: if (baseDir == null)
239: _baseURL = null;
240: else
241: try {
242: _baseURL = FileOps.toURL(baseDir);
243: } catch (MalformedURLException ex) {
244: throw new UnexpectedException(ex);
245: }
246:
247: // Load contents page
248: if (indexUrl == null)
249: _displayContentsError(null);
250: else
251: try {
252: _contentsDocPane.setPage(indexUrl);
253: if (_baseURL != null)
254: ((HTMLDocument) _contentsDocPane.getDocument())
255: .setBase(_baseURL);
256: } catch (IOException ioe) {
257: // Show some error page?
258: _displayContentsError(indexUrl, ioe);
259: }
260:
261: if (introUrl == null)
262: _displayMainError(null);
263: else {
264: _history = new HistoryList(introUrl);
265: _displayPage(introUrl);
266: _displayPage(introUrl);
267: }
268:
269: // Set all dimensions ----
270: setSize(FRAME_WIDTH, FRAME_HEIGHT);
271: MainFrame.setPopupLoc(this , null);
272: }
273:
274: /** Hides the navigation panel on the left. Cannot currently be undone. */
275: protected void _hideNavigationPane() {
276: _splitPaneHolder.remove(_splitPane);
277: _splitPaneHolder.add(_mainScroll);
278: }
279:
280: private void _resetMainPane() {
281: _linkError = false;
282:
283: _mainDocPane = new JEditorPane();
284: _mainDocPane.setEditable(false);
285: for (int i = 0; i < _hyperlinkListeners.size(); i++) {
286: _mainDocPane.addHyperlinkListener(_hyperlinkListeners
287: .get(i));
288: }
289: _displayPage(_lastURL);
290:
291: _splitPane.setRightComponent(new BorderlessScrollPane(
292: _mainDocPane));
293: _splitPane.setDividerLocation(LEFT_PANEL_WIDTH);
294: }
295:
296: /** Displays the given URL in the main pane. Changed to private, because of history system.
297: * @param url URL to display
298: */
299: private void _displayPage(URL url) {
300: if (url == null)
301: return;
302: try {
303: _mainDocPane.setPage(url);
304: if (_baseURL != null) {
305: ((HTMLDocument) _contentsDocPane.getDocument())
306: .setBase(_baseURL);
307: }
308: _lastURL = url;
309: } catch (IOException ioe) {
310: String path = url.getPath();
311: try {
312: URL newURL = new URL(_baseURL + path);
313: _mainDocPane.setPage(newURL);
314: if (_baseURL != null) {
315: ((HTMLDocument) _contentsDocPane.getDocument())
316: .setBase(_baseURL);
317: }
318: _lastURL = newURL;
319: } catch (IOException ioe2) {
320: // Show some error page?
321: _displayMainError(url, ioe2);
322: //System.err.println("couldn't find url: " + url);
323: }
324: }
325: }
326:
327: /** Prints an error indicating that the HTML file to load in the main pane could not be found. */
328: private void _displayMainError(URL url) {
329: if (!_linkError) {
330: _linkError = true;
331: _mainDocPane.setText(getErrorText(url));
332: } else
333: _resetMainPane();
334: }
335:
336: /** Prints an error indicating that the HTML file to load in the main pane could not be found
337: */
338: private void _displayMainError(URL url, Exception ex) {
339: if (!_linkError) {
340: _linkError = true;
341: _mainDocPane.setText(getErrorText(url) + "\n" + ex);
342: } else
343: _resetMainPane();
344: }
345:
346: /**
347: * Prints an error indicating that the HTML file to load in the contentes pane
348: * could not be found
349: */
350: private void _displayContentsError(URL url) {
351: _contentsDocPane.setText(getErrorText(url));
352: }
353:
354: /** Prints an error indicating that the HTML file to load in the contentes pane could not be found. */
355: private void _displayContentsError(URL url, Exception ex) {
356: _contentsDocPane.setText(getErrorText(url) + "\n" + ex);
357: }
358:
359: /** This method returns the error text to display when something goes wrong. */
360: protected String getErrorText(URL url) {
361: return "Could not load the specified URL: " + url;
362: }
363:
364: public void jumpTo(URL url) {
365: _history = new HistoryList(url, _history); // current history is prev for this node
366:
367: _backAction.setEnabled(true); // now we can back up.
368: _forwardAction.setEnabled(false); // can't go any more forward
369: // (any applicable previous forward info is lost) because you nuked the forward list
370: _displayPage(url);
371: }
372: }
|