Adding JMCR-Stable version
[Benchmarks_CSolver.git] / JMCR-Stable / real-world application / jigsaw / src / org / w3c / tools / forms / RangedIntegerField.java
diff --git a/JMCR-Stable/real-world application/jigsaw/src/org/w3c/tools/forms/RangedIntegerField.java b/JMCR-Stable/real-world application/jigsaw/src/org/w3c/tools/forms/RangedIntegerField.java
new file mode 100644 (file)
index 0000000..3a17fde
--- /dev/null
@@ -0,0 +1,108 @@
+// RangedIntegerField.java\r
+// $Id: RangedIntegerField.java,v 1.1 2010/06/15 12:27:21 smhuang Exp $\r
+// (c) COPYRIGHT MIT and INRIA, 1996.\r
+// Please first read the full copyright statement in file COPYRIGHT.html\r
+\r
+package org.w3c.tools.forms ;\r
+\r
+import java.awt.BorderLayout;\r
+import java.awt.Component;\r
+import java.awt.Container;\r
+import java.awt.Event;\r
+import java.awt.Insets;\r
+import java.awt.Panel;\r
+import java.awt.Scrollbar;\r
+import java.awt.TextComponent;\r
+import java.awt.TextField;\r
+\r
+class RangedIntegerFieldEditor extends Panel {\r
+    RangedIntegerField field = null ;\r
+    TextField text   = null ;\r
+    Scrollbar slider = null ;\r
+    int       lo     = Integer.MIN_VALUE ;\r
+    int       hi     = Integer.MAX_VALUE ;\r
+\r
+    public boolean action (Event evt, Object arg) {\r
+       try {\r
+           Integer ival = new Integer(Integer.parseInt(text.getText()));\r
+           if ( ! field.acceptChange(ival) )\r
+               text.setText(field.getValue().toString()) ;\r
+           return true ;\r
+       } catch (NumberFormatException ex) {\r
+           // This should never happen!\r
+           throw new RuntimeException ("implementation bug !");\r
+       }\r
+    }\r
+\r
+    public boolean handleEvent (Event evt) {\r
+       if ( evt.target instanceof Scrollbar ) {\r
+           text.setText(String.valueOf(slider.getValue()));\r
+           return true ;\r
+       } else {\r
+           return super.handleEvent(evt) ;\r
+       }\r
+    }\r
+\r
+    public boolean keyDown (Event evt, int key) {\r
+       if ( evt.target instanceof TextField ) {\r
+           switch (key) {\r
+             case 9:\r
+             case 10:\r
+                 action(evt, evt.arg) ;\r
+                 field.manager.nextField() ;\r
+                 return true ;\r
+             case '0': case '1': case '2': case '3': case '4':\r
+             case '5': case '6': case '7': case '8': case '9':\r
+             case Event.LEFT: case Event.RIGHT: case 96: case 127:\r
+                 return super.keyDown(evt, key) ;\r
+             default:\r
+                 return true ;\r
+           }\r
+       } else {\r
+           return super.keyDown(evt, key) ;\r
+       }\r
+    }\r
+\r
+    public Insets insets() {\r
+       return new Insets(5, 5, 5, 8) ;\r
+    }\r
+\r
+    RangedIntegerFieldEditor(RangedIntegerField field, int lo, int hi, int v) {\r
+       super() ;\r
+       this.field = field ;\r
+       BorderLayout bl = new BorderLayout() ;\r
+       setLayout(bl) ;\r
+       // Add the text:\r
+       text = new TextField("0") ;\r
+       add ("North", text) ;\r
+       // Add the slider:\r
+       slider = new Scrollbar(Scrollbar.HORIZONTAL, 0, 100, lo, hi) ;\r
+       add ("South", slider) ;\r
+    }\r
+}\r
+\r
+public class RangedIntegerField extends IntegerField {\r
+    int hi = Integer.MAX_VALUE ;\r
+    int lo = Integer.MIN_VALUE ;\r
+    RangedIntegerFieldEditor editor = null ;\r
+\r
+    /**\r
+     * Get an editor for this field.\r
+     */\r
+\r
+    public Component getEditor() {\r
+       if ( editor == null )\r
+           editor = new RangedIntegerFieldEditor(this, lo, hi, getIntValue());\r
+       return editor ;\r
+    }\r
+\r
+    public RangedIntegerField(FormManager manager\r
+                             , String name, String title\r
+                             , int lo, int hi, int val)\r
+       throws IllegalFieldValueException\r
+    {\r
+       super(manager, name, title, val) ;\r
+       this.lo = lo ;\r
+       this.hi = hi ;\r
+    }\r
+}\r