Adding JMCR-Stable version

[Benchmarks_CSolver.git] / JMCR-Stable / real-world application / jigsaw / src / org / w3c / jigadmin / editors / MyHTMLEditorKit.java

diff --git a/JMCR-Stable/real-world application/jigsaw/src/org/w3c/jigadmin/editors/MyHTMLEditorKit.java b/JMCR-Stable/real-world application/jigsaw/src/org/w3c/jigadmin/editors/MyHTMLEditorKit.java
new file mode 100644 (file)
index 0000000..bf8b3f4
--- /dev/null
+++ b/JMCR-Stable/real-world application/jigsaw/src/org/w3c/jigadmin/editors/MyHTMLEditorKit.java
@@ -0,0 +1,133 @@
+// MyHTMLEditorKit.java\r
+// $Id: MyHTMLEditorKit.java,v 1.1 2010/06/15 12:25:52 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 javax.swing.JEditorPane;\r
+import javax.swing.text.Document;\r
+import javax.swing.text.AttributeSet;\r
+import javax.swing.text.Element;\r
+import javax.swing.text.html.HTML;\r
+import javax.swing.text.html.HTMLEditorKit;\r
+import javax.swing.text.html.HTMLDocument;\r
+import javax.swing.event.HyperlinkEvent;\r
+import javax.swing.event.MouseInputAdapter;\r
+\r
+import java.awt.event.MouseEvent;\r
+import java.awt.Point;\r
+\r
+import java.io.Serializable;\r
+\r
+import java.net.URL;\r
+import java.net.MalformedURLException;\r
+\r
+/**\r
+ * A special HTMLEditorKit that handle mouse event.\r
+ */\r
+public class MyHTMLEditorKit extends HTMLEditorKit {\r
+\r
+    public static final int JUMP = 0;\r
+    public static final int MOVE = 1;\r
+\r
+    LinkController myController = new LinkController();\r
+\r
+    /**\r
+     * Called when the kit is being installed into the a JEditorPane.\r
+     * @param c the JEditorPane.\r
+     */\r
+    public void install(JEditorPane c) {\r
+       c.addMouseListener(myController);\r
+       c.addMouseMotionListener(myController);\r
+    }\r
+\r
+    /**\r
+     * Our MouseListener.\r
+     */\r
+    public static class LinkController extends MouseInputAdapter \r
+       implements Serializable \r
+    {\r
+\r
+       URL currentUrl = null;\r
+\r
+       public void mouseClicked(MouseEvent e) {\r
+           JEditorPane editor = (JEditorPane) e.getSource();\r
+\r
+           if (! editor.isEditable()) {\r
+               Point pt = new Point(e.getX(), e.getY());\r
+               try {\r
+                   int pos = editor.viewToModel(pt);\r
+                   if (pos >= 0) {\r
+                       activateLink(pos, editor, JUMP);\r
+                   }\r
+               } catch (IllegalArgumentException iae) {}\r
+           }\r
+       }\r
+\r
+       public void mouseMoved(MouseEvent e) {\r
+           JEditorPane editor = (JEditorPane) e.getSource();\r
+\r
+           if (! editor.isEditable()) {\r
+               Point pt = new Point(e.getX(), e.getY());\r
+               try {\r
+                   int pos = editor.viewToModel(pt);\r
+                   if (pos >= 0) {\r
+                       activateLink(pos, editor, MOVE);\r
+                   }\r
+               } catch (IllegalArgumentException iae) {}\r
+           }\r
+       }\r
+\r
+       protected void activateLink(int pos, JEditorPane html, int type) {\r
+           Document doc = html.getDocument();\r
+           if (doc instanceof HTMLDocument) {\r
+               HTMLDocument hdoc = (HTMLDocument) doc;\r
+               Element e = hdoc.getCharacterElement(pos);\r
+               AttributeSet a = e.getAttributes();\r
+               AttributeSet anchor = \r
+                   (AttributeSet) a.getAttribute(HTML.Tag.A);\r
+               String href = (anchor != null) ? \r
+                   (String) anchor.getAttribute(HTML.Attribute.HREF) : null;\r
+               boolean shouldExit = false;\r
+\r
+               HyperlinkEvent linkEvent = null;\r
+               if (href != null) {\r
+                   URL u;\r
+                   try {\r
+                       u = new URL(hdoc.getBase(), href);\r
+                   } catch (MalformedURLException m) {\r
+                       u = null;\r
+                   }\r
+\r
+                   if ((type == MOVE) && (!u.equals(currentUrl))) {\r
+                       linkEvent =  new HyperlinkEvent(html, \r
+                                       HyperlinkEvent.EventType.ENTERED, \r
+                                                       u, href);\r
+                       currentUrl = u;\r
+                   }\r
+                   else if (type == JUMP) {\r
+                       linkEvent = new HyperlinkEvent(html, \r
+                                      HyperlinkEvent.EventType.ACTIVATED, \r
+                                                      u, href);\r
+                       shouldExit = true;\r
+                   }\r
+                   else {\r
+                       return;\r
+                   }\r
+                   html.fireHyperlinkUpdate(linkEvent);\r
+               }\r
+               else if (currentUrl != null) {\r
+                   shouldExit = true;\r
+               }\r
+               if (shouldExit) {\r
+                   linkEvent = new HyperlinkEvent(html,\r
+                                          HyperlinkEvent.EventType.EXITED,\r
+                                                  currentUrl, null);\r
+                   html.fireHyperlinkUpdate(linkEvent);\r
+                   currentUrl = null;\r
+               }\r
+           }\r
+       }\r
+    }\r
+}\r