--- /dev/null
+// MiniBrowser.java\r
+// $Id: MiniBrowser.java,v 1.1 2010/06/15 12:25:51 smhuang Exp $\r
+// (c) COPYRIGHT MIT, INRIA and Keio, 1999.\r
+// Please first read the full copyright statement in file COPYRIGHT.html\r
+\r
+package org.w3c.jigadmin.editors;\r
+\r
+import java.awt.Cursor;\r
+import java.awt.GridLayout;\r
+import java.awt.BorderLayout;\r
+import java.awt.Container;\r
+import java.awt.event.WindowAdapter;\r
+import java.awt.event.WindowEvent;\r
+import java.awt.event.ActionEvent;\r
+import java.awt.event.ActionListener;\r
+\r
+import javax.swing.JPanel;\r
+import javax.swing.JLabel;\r
+import javax.swing.JButton;\r
+import javax.swing.JScrollPane;\r
+import javax.swing.JEditorPane;\r
+import javax.swing.BorderFactory;\r
+import javax.swing.JTextField;\r
+import javax.swing.event.HyperlinkEvent;\r
+import javax.swing.event.HyperlinkListener;\r
+\r
+import java.net.URL;\r
+import java.net.MalformedURLException;\r
+\r
+import java.util.Vector;\r
+import java.util.NoSuchElementException;\r
+\r
+import java.io.IOException;\r
+\r
+import org.w3c.jigadmin.widgets.ClosableFrame;\r
+\r
+import org.w3c.tools.widgets.Utilities;\r
+\r
+/**\r
+ * A mini HTML browser.\r
+ * @version $Revision: 1.1 $\r
+ * @author Benoît Mahé (bmahe@w3.org)\r
+ */\r
+public class MiniBrowser extends ClosableFrame {\r
+\r
+ private static MiniBrowser mbrowser = null;\r
+\r
+ private Vector prevurls = null;\r
+ private Vector nexturls = null;\r
+\r
+ protected final static String NEXT_AC = "next";\r
+ protected final static String PREV_AC = "prev";\r
+ protected final static String TEXT_AC = "text";\r
+\r
+ protected JLabel statusBar = null;\r
+ protected JTextField urlField = null;\r
+ protected JEditorPane editor = null;\r
+ protected JButton next_B = null;\r
+ protected JButton prev_B = null;\r
+\r
+ protected History history = null;\r
+ protected URL currentURL = null;\r
+\r
+ /**\r
+ * The browser history.\r
+ */\r
+ class History {\r
+ private Vector prevurls = null;\r
+ private Vector nexturls = null;\r
+\r
+ protected synchronized void add(Object obj) {\r
+ prevurls.addElement(obj);\r
+ nexturls.clear();\r
+ prev_B.setEnabled(true);\r
+ next_B.setEnabled(false);\r
+ }\r
+\r
+ protected synchronized Object getPrev(Object current) \r
+ throws NoSuchElementException\r
+ {\r
+ Object prev = prevurls.lastElement();\r
+ prevurls.removeElementAt(prevurls.size()-1);\r
+ nexturls.addElement(current);\r
+ if (prevurls.size() > 0)\r
+ prev_B.setEnabled(true);\r
+ else\r
+ prev_B.setEnabled(false);\r
+ next_B.setEnabled(true);\r
+ return prev;\r
+ }\r
+\r
+ protected synchronized Object getNext(Object current) \r
+ throws NoSuchElementException\r
+ {\r
+ Object next = nexturls.lastElement();\r
+ nexturls.removeElementAt(nexturls.size()-1);\r
+ prevurls.addElement(current);\r
+ prev_B.setEnabled(true);\r
+ if (nexturls.size() > 0)\r
+ next_B.setEnabled(true);\r
+ else\r
+ next_B.setEnabled(false);\r
+ return next;\r
+ }\r
+\r
+ History(){\r
+ prevurls = new Vector(10);\r
+ nexturls = new Vector(10);\r
+ }\r
+ }\r
+\r
+ /**\r
+ * Our internal HyperLinkListener.\r
+ */\r
+ HyperlinkListener hll = new HyperlinkListener() {\r
+ public void hyperlinkUpdate(HyperlinkEvent he) {\r
+ HyperlinkEvent.EventType type = he.getEventType();\r
+\r
+ if (type == HyperlinkEvent.EventType.ENTERED) {\r
+ editor.setCursor(Cursor.\r
+ getPredefinedCursor(Cursor.HAND_CURSOR));\r
+ statusBar.setText(he.getURL().toString());\r
+ }\r
+ else if (type == HyperlinkEvent.EventType.EXITED) {\r
+ editor.setCursor(Cursor.getDefaultCursor());\r
+ statusBar.setText(" ");\r
+ }\r
+ else {\r
+ try {\r
+ if (currentURL != null)\r
+ history.add(currentURL);\r
+ setPage(he.getURL());\r
+ if (urlField != null) {\r
+ urlField.setText(he.getURL().toString());\r
+ }\r
+ } catch (Exception e) {\r
+ e.printStackTrace();\r
+ }\r
+ }\r
+ }\r
+ };\r
+\r
+ /**\r
+ * Our internal ActionListener.\r
+ */\r
+ ActionListener al = new ActionListener() {\r
+ public void actionPerformed(ActionEvent ae) {\r
+ String command = ae.getActionCommand();\r
+ if (command.equals(PREV_AC)) {\r
+ try {\r
+ setPage((URL)history.getPrev(currentURL));\r
+ } catch (NoSuchElementException ex) {\r
+ } catch (IOException io) {\r
+ io.printStackTrace();\r
+ }\r
+ } else if (command.equals(NEXT_AC)) {\r
+ try {\r
+ setPage((URL)history.getNext(currentURL));\r
+ } catch (NoSuchElementException ex) {\r
+ } catch (IOException io) {\r
+ io.printStackTrace();\r
+ }\r
+ } else if (command.equals(TEXT_AC)) {\r
+ \r
+ history.add(currentURL);\r
+ try {\r
+ setPage(urlField.getText());\r
+ } catch (Exception ex) {\r
+ ex.printStackTrace();\r
+ }\r
+ }\r
+ }\r
+ };\r
+\r
+ protected void build(String url) {\r
+ Container cont = getContentPane();\r
+ cont.setLayout(new BorderLayout());\r
+\r
+ prev_B = new JButton("Prev");\r
+ prev_B.setActionCommand(PREV_AC);\r
+ prev_B.addActionListener(al);\r
+ prev_B.setEnabled(false);\r
+ next_B = new JButton("Next");\r
+ next_B.setActionCommand(NEXT_AC);\r
+ next_B.addActionListener(al);\r
+ next_B.setEnabled(false);\r
+ JPanel pb = new JPanel(new GridLayout(1,2));\r
+ pb.add(prev_B);\r
+ pb.add(next_B);\r
+\r
+ urlField = new JTextField(40);\r
+ urlField.setActionCommand(TEXT_AC);\r
+ urlField.addActionListener(al);\r
+ urlField.setBorder(BorderFactory.createLoweredBevelBorder());\r
+ JLabel location = new JLabel(" Location:");\r
+ JPanel urlp = new JPanel(new BorderLayout());\r
+ urlp.add(location, BorderLayout.WEST);\r
+ urlp.add(urlField, BorderLayout.CENTER);\r
+\r
+ JPanel bar = new JPanel(new BorderLayout());\r
+ bar.add(pb, BorderLayout.WEST);\r
+ bar.add(urlp, BorderLayout.CENTER);\r
+ bar.setBorder(BorderFactory.createRaisedBevelBorder());\r
+\r
+ statusBar = new JLabel(url);\r
+ statusBar.setFont(Utilities.smallFont);\r
+ statusBar.setBorder(BorderFactory.createRaisedBevelBorder());\r
+\r
+ editor = new JEditorPane();\r
+ editor.setEditable(false);\r
+ editor.setEditorKitForContentType("text/html", new MyHTMLEditorKit());\r
+ editor.addHyperlinkListener(hll);\r
+\r
+ cont.add(bar, BorderLayout.NORTH);\r
+ cont.add(new JScrollPane(editor), BorderLayout.CENTER);\r
+ cont.add(statusBar, BorderLayout.SOUTH);\r
+ }\r
+\r
+ /**\r
+ * Constructor.\r
+ * @param url The url to browse\r
+ * @param title the frame Title\r
+ * @exception MalformedURLException if the URL is an invalid URL.\r
+ * @exception IOException if an IO error occurs.\r
+ */\r
+ public MiniBrowser(String url, String title) \r
+ throws MalformedURLException, IOException\r
+ {\r
+ super(title);\r
+ history = new History();\r
+ build(url);\r
+ setPage(url);\r
+ }\r
+\r
+ /**\r
+ * Constructor.\r
+ * @param title the frame Title\r
+ * @exception MalformedURLException if the URL is an invalid URL.\r
+ * @exception IOException if an IO error occurs.\r
+ */\r
+ public MiniBrowser(String title)\r
+ throws MalformedURLException, IOException\r
+ {\r
+ super(title);\r
+ history = new History();\r
+ build("");\r
+ }\r
+\r
+ /**\r
+ * The frame has been closed.\r
+ */\r
+ protected void close() {\r
+ mbrowser = null;\r
+ }\r
+\r
+ /**\r
+ * Set the current URL.\r
+ * @param url the new current url.\r
+ * @exception MalformedURLException if the URL is an invalid URL.\r
+ * @exception IOException if an IO error occurs.\r
+ */\r
+ public void setPage(String url)\r
+ throws MalformedURLException, IOException\r
+ {\r
+ currentURL = new URL(url);\r
+ editor.setPage(currentURL);\r
+ urlField.setText(url);\r
+ }\r
+\r
+ /**\r
+ * Set the current URL.\r
+ * @param url the new current url.\r
+ * @exception IOException if an IO error occurs.\r
+ */\r
+ public void setPage(URL url)\r
+ throws IOException\r
+ {\r
+ currentURL = url;\r
+ editor.setPage(url);\r
+ urlField.setText(url.toExternalForm());\r
+ }\r
+\r
+ /**\r
+ * Show the current MiniBrowser for the given URL.\r
+ * @param url the new current url.\r
+ * @param title the frame title.\r
+ * @exception MalformedURLException if the URL is an invalid URL.\r
+ * @exception IOException if an IO error occurs.\r
+ */\r
+ public static void showDocumentationURL(String url, String title) \r
+ throws MalformedURLException, IOException\r
+ {\r
+ if (mbrowser == null) {\r
+ mbrowser = new MiniBrowser(url, title);\r
+ mbrowser.setSize(600, 600);\r
+ mbrowser.setVisible(true);\r
+ } else {\r
+ mbrowser.history.add(mbrowser.currentURL);\r
+ mbrowser.setPage(url);\r
+ }\r
+ }\r
+\r
+ public static void main(String args[]) {\r
+ try {\r
+\r
+ MiniBrowser browser = null;\r
+ if (args.length > 0) \r
+ browser = new MiniBrowser(args[0], "Mini Browser");\r
+ else\r
+ browser = new MiniBrowser("Mini Browser");\r
+\r
+ browser.addWindowListener(new WindowAdapter() {\r
+ public void windowClosing(WindowEvent e) {\r
+ System.exit(0);\r
+ }\r
+ });\r
+\r
+ browser.setSize(600, 600);\r
+ browser.setVisible(true);\r
+ } catch (Exception ex) {\r
+ ex.printStackTrace();\r
+ }\r
+ }\r
+\r
+}\r
projects / Benchmarks_CSolver.git / blobdiff