[isidorus-cvs] r554 - branches/gdl-frontend/src/anaToMia/GDL_Widgets/src/us/isidor/gdl/anaToMia/Widgets/base
Author: lgiessmann Date: Sun Jul 3 23:00:30 2011 New Revision: 554
Log: gdl-frontend: Widgets: started to implement style setters for the GDL/CSS pseudo style classes
Modified: branches/gdl-frontend/src/anaToMia/GDL_Widgets/src/us/isidor/gdl/anaToMia/Widgets/base/GdlVisibleObject.java
Modified: branches/gdl-frontend/src/anaToMia/GDL_Widgets/src/us/isidor/gdl/anaToMia/Widgets/base/GdlVisibleObject.java ============================================================================== --- branches/gdl-frontend/src/anaToMia/GDL_Widgets/src/us/isidor/gdl/anaToMia/Widgets/base/GdlVisibleObject.java Fri Jul 1 15:01:50 2011 (r553) +++ branches/gdl-frontend/src/anaToMia/GDL_Widgets/src/us/isidor/gdl/anaToMia/Widgets/base/GdlVisibleObject.java Sun Jul 3 23:00:30 2011 (r554) @@ -1100,321 +1100,481 @@ // sets the vertical-align style property of this element by using the GWT DOM class - public void setVerticalAlign(VerticalAlign value){ + public void setVerticalAlign(VerticalAlign value, String styleClass){ if(value != null){ - DOM.setStyleAttribute(this.getElement(), "verticalAlign", value.getCssName()); + if(styleClass == null){ + DOM.setStyleAttribute(this.getElement(), "verticalAlign", value.getCssName()); + } else { + // TODO: implement + } } } // sets the margin style property of this element by using the GWT DOM class - public void setMargin(NumUnitValue value){ + public void setMargin(NumUnitValue value, String styleClass){ if(value != null){ - DOM.setStyleAttribute(this.getElement(), "margin", value.getCssValue()); + if(styleClass == null){ + DOM.setStyleAttribute(this.getElement(), "margin", value.getCssValue()); + } else { + // TODO: implement + } } } // sets the margin-top style property of this element by using the GWT DOM class - public void setMarginTop(NumUnitValue value){ + public void setMarginTop(NumUnitValue value, String styleClass){ if(value != null){ - DOM.setStyleAttribute(this.getElement(), "marginTop", value.getCssValue()); + if(styleClass == null){ + DOM.setStyleAttribute(this.getElement(), "marginTop", value.getCssValue()); + } else { + // TODO: implement + } } } // sets the margin-right style property of this element by using the GWT DOM class - public void setMarginRight(NumUnitValue value){ + public void setMarginRight(NumUnitValue value, String styleClass){ if(value != null){ - DOM.setStyleAttribute(this.getElement(), "marginRight", value.getCssValue()); + if(styleClass == null){ + DOM.setStyleAttribute(this.getElement(), "marginRight", value.getCssValue()); + } else { + // TODO: implement + } } } // sets the margin-bottom style property of this element by using the GWT DOM class - public void setMarginBottom(NumUnitValue value){ + public void setMarginBottom(NumUnitValue value, String styleClass){ if(value != null){ - DOM.setStyleAttribute(this.getElement(), "marginBottom", value.getCssValue()); + if(styleClass == null){ + DOM.setStyleAttribute(this.getElement(), "marginBottom", value.getCssValue()); + } else { + // TODO: implement + } } } // sets the margin-left style property of this element by using the GWT DOM class - public void setMarginLeft(NumUnitValue value){ + public void setMarginLeft(NumUnitValue value, String styleClass){ if(value != null){ - DOM.setStyleAttribute(this.getElement(), "marginLeft", value.getCssValue()); + if(styleClass == null){ + DOM.setStyleAttribute(this.getElement(), "marginLeft", value.getCssValue()); + } else { + // TODO: implement + } } } // sets the border-color style property of this element by using the GWT DOM class - public void setBorderColor(ColorValue value){ + public void setBorderColor(ColorValue value, String styleClass){ if(value != null){ - DOM.setStyleAttribute(this.getElement(), "borderColor", value.getCssValue()); + if(styleClass == null){ + DOM.setStyleAttribute(this.getElement(), "borderColor", value.getCssValue()); + } else { + // TODO: implement + } } }
// sets the border-top-color style property of this element by using the GWT DOM class - public void setBorderTopColor(ColorValue value){ + public void setBorderTopColor(ColorValue value, String styleClass){ if(value != null){ - DOM.setStyleAttribute(this.getElement(), "borderTopColor", value.getCssValue()); + if(styleClass == null){ + DOM.setStyleAttribute(this.getElement(), "borderTopColor", value.getCssValue()); + } else { + // TODO: implement + } } } // sets the border-right-color style property of this element by using the GWT DOM class - public void setBorderRightColor(ColorValue value){ + public void setBorderRightColor(ColorValue value, String styleClass){ if(value != null){ - DOM.setStyleAttribute(this.getElement(), "borderRightColor", value.getCssValue()); + if(styleClass == null){ + DOM.setStyleAttribute(this.getElement(), "borderRightColor", value.getCssValue()); + } else { + // TODO: implement + } } } // sets the border-bottom-color style property of this element by using the GWT DOM class - public void setBorderBottomColor(ColorValue value){ + public void setBorderBottomColor(ColorValue value, String styleClass){ if(value != null){ - DOM.setStyleAttribute(this.getElement(), "borderBottomColor", value.getCssValue()); + if(styleClass == null){ + DOM.setStyleAttribute(this.getElement(), "borderBottomColor", value.getCssValue()); + } else { + // TODO: implement + } } } // sets the border-left-color style property of this element by using the GWT DOM class - public void setBorderLeftColor(ColorValue value){ + public void setBorderLeftColor(ColorValue value, String styleClass){ if(value != null){ - DOM.setStyleAttribute(this.getElement(), "borderLeftColor", value.getCssValue()); + if(styleClass == null){ + DOM.setStyleAttribute(this.getElement(), "borderLeftColor", value.getCssValue()); + } else { + // TODO: implement + } } } // sets the border-style style property of this element by using the GWT DOM class - public void setBorderStyle(BorderStyleValue value){ + public void setBorderStyle(BorderStyleValue value, String styleClass){ if(value != null){ - DOM.setStyleAttribute(this.getElement(), "borderStyle", value.getCssValue()); + if(styleClass == null){ + DOM.setStyleAttribute(this.getElement(), "borderStyle", value.getCssValue()); + } else { + // TODO: implement + } } } // sets the border-top-style style property of this element by using the GWT DOM class - public void setBorderTopStyle(BorderStyleValue value){ + public void setBorderTopStyle(BorderStyleValue value, String styleClass){ if(value != null){ - DOM.setStyleAttribute(this.getElement(), "borderTopStyle", value.getCssValue()); + if(styleClass == null){ + DOM.setStyleAttribute(this.getElement(), "borderTopStyle", value.getCssValue()); + } else { + // TODO: implement + } } } // sets the border-right-style style property of this element by using the GWT DOM class - public void setBorderRightStyle(BorderStyleValue value){ + public void setBorderRightStyle(BorderStyleValue value, String styleClass){ if(value != null){ - DOM.setStyleAttribute(this.getElement(), "borderRightStyle", value.getCssValue()); + if(styleClass == null){ + DOM.setStyleAttribute(this.getElement(), "borderRightStyle", value.getCssValue()); + } else { + // TODO: implement + } } } // sets the border-bottom-style style property of this element by using the GWT DOM class - public void setBorderBottomStyle(BorderStyleValue value){ + public void setBorderBottomStyle(BorderStyleValue value, String styleClass){ if(value != null){ - DOM.setStyleAttribute(this.getElement(), "borderBottomStyle", value.getCssValue()); + if(styleClass == null){ + DOM.setStyleAttribute(this.getElement(), "borderBottomStyle", value.getCssValue()); + } else { + // TODO: implement + } } } // sets the border-left-style style property of this element by using the GWT DOM class - public void setBorderLeftStyle(BorderStyleValue value){ + public void setBorderLeftStyle(BorderStyleValue value, String styleClass){ if(value != null){ - DOM.setStyleAttribute(this.getElement(), "borderLeftStyle", value.getCssValue()); + if(styleClass == null){ + DOM.setStyleAttribute(this.getElement(), "borderLeftStyle", value.getCssValue()); + } else { + // TODO: implement + } } }
// sets the border-width style property of this element by using the GWT DOM class - public void setBorderWidth(AbsoluteNumValue value){ + public void setBorderWidth(AbsoluteNumValue value, String styleClass){ if(value != null){ - DOM.setStyleAttribute(this.getElement(), "borderWidth", value.getCssValue()); + if(styleClass == null){ + DOM.setStyleAttribute(this.getElement(), "borderWidth", value.getCssValue()); + } else { + // TODO: implement + } } } // sets the border-width style property of this element by using the GWT DOM class - public void setBorderTopWidth(AbsoluteNumValue value){ + public void setBorderTopWidth(AbsoluteNumValue value, String styleClass){ if(value != null){ - DOM.setStyleAttribute(this.getElement(), "borderTopWidth", value.getCssValue()); + if(styleClass == null){ + DOM.setStyleAttribute(this.getElement(), "borderTopWidth", value.getCssValue()); + } else { + // TODO: implement + } } } // sets the border-width style property of this element by using the GWT DOM class - public void setBorderRightWidth(AbsoluteNumValue value){ + public void setBorderRightWidth(AbsoluteNumValue value, String styleClass){ if(value != null){ - DOM.setStyleAttribute(this.getElement(), "borderRightWidth", value.getCssValue()); + if(styleClass == null){ + DOM.setStyleAttribute(this.getElement(), "borderRightWidth", value.getCssValue()); + } else { + // TODO: implement + } } } // sets the border-width style property of this element by using the GWT DOM class - public void setBorderBottomWidth(AbsoluteNumValue value){ + public void setBorderBottomWidth(AbsoluteNumValue value, String styleClass){ if(value != null){ - DOM.setStyleAttribute(this.getElement(), "borderBottomWidth", value.getCssValue()); + if(styleClass == null){ + DOM.setStyleAttribute(this.getElement(), "borderBottomWidth", value.getCssValue()); + } else { + // TODO: implement + } } } // sets the border-width style property of this element by using the GWT DOM class - public void setBorderLeftWidth(AbsoluteNumValue value){ + public void setBorderLeftWidth(AbsoluteNumValue value, String styleClass){ if(value != null){ - DOM.setStyleAttribute(this.getElement(), "borderLeftWidth", value.getCssValue()); + if(styleClass == null){ + DOM.setStyleAttribute(this.getElement(), "borderLeftWidth", value.getCssValue()); + } else { + // TODO: implement + } } } // sets the border-radius style property of this element by using the GWT DOM class - public void setBorderRadius(NumUnitValue value){ + public void setBorderRadius(NumUnitValue value, String styleClass){ if(value != null){ - DOM.setStyleAttribute(this.getElement(), "borderRadius", value.getCssValue()); + if(styleClass == null){ + DOM.setStyleAttribute(this.getElement(), "borderRadius", value.getCssValue()); + } else { + // TODO: implement + } } } // sets the border-top-right-radius style property of this element by using the GWT DOM class - public void setBorderTopRightRadius(NumUnitValue value){ + public void setBorderTopRightRadius(NumUnitValue value, String styleClass){ if(value != null){ - DOM.setStyleAttribute(this.getElement(), "borderTopRightRadius", value.getCssValue()); + if(styleClass == null){ + DOM.setStyleAttribute(this.getElement(), "borderTopRightRadius", value.getCssValue()); + } else { + // TODO: implement + } } } // sets the border-bottom-right-radius style property of this element by using the GWT DOM class - public void setBorderBottomRightRadius(NumUnitValue value){ + public void setBorderBottomRightRadius(NumUnitValue value, String styleClass){ if(value != null){ - DOM.setStyleAttribute(this.getElement(), "borderBottomRightRadius", value.getCssValue()); + if(styleClass == null){ + DOM.setStyleAttribute(this.getElement(), "borderBottomRightRadius", value.getCssValue()); + } else { + // TODO: implement + } } } // sets the border-bottom-left-radius style property of this element by using the GWT DOM class - public void setBorderBottomLeftRadius(NumUnitValue value){ + public void setBorderBottomLeftRadius(NumUnitValue value, String styleClass){ if(value != null){ - DOM.setStyleAttribute(this.getElement(), "borderBottomLeftRadius", value.getCssValue()); + if(styleClass == null){ + DOM.setStyleAttribute(this.getElement(), "borderBottomLeftRadius", value.getCssValue()); + } else { + // TODO: implement + } } } // sets the border-top-left-radius style property of this element by using the GWT DOM class - public void setBorderTopLeftRadius(NumUnitValue value){ + public void setBorderTopLeftRadius(NumUnitValue value, String styleClass){ if(value != null){ - DOM.setStyleAttribute(this.getElement(), "borderTopLeftRadius", value.getCssValue()); + if(styleClass == null){ + DOM.setStyleAttribute(this.getElement(), "borderTopLeftRadius", value.getCssValue()); + } else { + // TODO: implement + } } } // sets the padding style property of this element by using the GWT DOM class - public void setPadding(NumUnitValue value){ + public void setPadding(NumUnitValue value, String styleClass){ if(value != null){ - DOM.setStyleAttribute(this.getElement(), "padding", value.getCssValue()); + if(styleClass == null){ + DOM.setStyleAttribute(this.getElement(), "padding", value.getCssValue()); + } else { + // TODO: implement + } } } // sets the padding-top style property of this element by using the GWT DOM class - public void setPaddingTop(NumUnitValue value){ + public void setPaddingTop(NumUnitValue value, String styleClass){ if(value != null){ - DOM.setStyleAttribute(this.getElement(), "paddingTop", value.getCssValue()); + if(styleClass == null){ + DOM.setStyleAttribute(this.getElement(), "paddingTop", value.getCssValue()); + } else { + // TODO: implement + } } } // sets the padding-right style property of this element by using the GWT DOM class - public void setPaddingRight(NumUnitValue value){ + public void setPaddingRight(NumUnitValue value, String styleClass){ if(value != null){ - DOM.setStyleAttribute(this.getElement(), "paddingRight", value.getCssValue()); + if(styleClass == null){ + DOM.setStyleAttribute(this.getElement(), "paddingRight", value.getCssValue()); + } else { + // TODO: implement + } } } // sets the padding-bottom style property of this element by using the GWT DOM class - public void setPaddingBottom(NumUnitValue value){ + public void setPaddingBottom(NumUnitValue value, String styleClass){ if(value != null){ - DOM.setStyleAttribute(this.getElement(), "paddingBottom", value.getCssValue()); + if(styleClass == null){ + DOM.setStyleAttribute(this.getElement(), "paddingBottom", value.getCssValue()); + } else { + // TODO: implement + } } } // sets the padding-left style property of this element by using the GWT DOM class - public void setPaddingLeft(NumUnitValue value){ + public void setPaddingLeft(NumUnitValue value, String styleClass){ if(value != null){ - DOM.setStyleAttribute(this.getElement(), "paddingLeft", value.getCssValue()); + if(styleClass == null){ + DOM.setStyleAttribute(this.getElement(), "paddingLeft", value.getCssValue()); + } else { + // TODO: implement + } } }
// sets the width style property of this element by using the GWT DOM class - public void setWidth(AutoNumUnitValue value){ + public void setWidth(AutoNumUnitValue value, String styleClass){ if(value != null){ - DOM.setStyleAttribute(this.getElement(), "width", value.getCssValue()); + if(styleClass == null){ + DOM.setStyleAttribute(this.getElement(), "width", value.getCssValue()); + } else { + // TODO: implement + } } } // sets the min-width style property of this element by using the GWT DOM class - public void setMinWidth(AutoNumUnitValue value){ + public void setMinWidth(AutoNumUnitValue value, String styleClass){ if(value != null){ - DOM.setStyleAttribute(this.getElement(), "minWidth", value.getCssValue()); + if(styleClass == null){ + DOM.setStyleAttribute(this.getElement(), "minWidth", value.getCssValue()); + } else { + // TODO: implement + } } } // sets the max-width style property of this element by using the GWT DOM class - public void setMaxWidth(AutoNumUnitValue value){ + public void setMaxWidth(AutoNumUnitValue value, String styleClass){ if(value != null){ - DOM.setStyleAttribute(this.getElement(), "maxWidth", value.getCssValue()); + if(styleClass == null){ + DOM.setStyleAttribute(this.getElement(), "maxWidth", value.getCssValue()); + } else { + // TODO: implement + } } } // sets the height style property of this element by using the GWT DOM class - public void setHeight(AutoNumUnitValue value){ + public void setHeight(AutoNumUnitValue value, String styleClass){ if(value != null){ + if(styleClass == null){ DOM.setStyleAttribute(this.getElement(), "height", value.getCssValue()); + } else { + // TODO: implement + } } } // sets the min-height style property of this element by using the GWT DOM class - public void setMinHeight(AutoNumUnitValue value){ + public void setMinHeight(AutoNumUnitValue value, String styleClass){ if(value != null){ - DOM.setStyleAttribute(this.getElement(), "minHeight", value.getCssValue()); + if(styleClass == null){ + DOM.setStyleAttribute(this.getElement(), "minHeight", value.getCssValue()); + } else { + // TODO: implement + } } } // sets the max-height style property of this element by using the GWT DOM class - public void setMaxHeight(AutoNumUnitValue value){ + public void setMaxHeight(AutoNumUnitValue value, String styleClass){ if(value != null){ - DOM.setStyleAttribute(this.getElement(), "maxHeight", value.getCssValue()); + if(styleClass == null){ + DOM.setStyleAttribute(this.getElement(), "maxHeight", value.getCssValue()); + } else { + // TODO: implement + } } } // sets the cursor style property of this element by using the GWT DOM class - public void setCursor(CursorValue value){ + public void setCursor(CursorValue value, String styleClass){ if(value != null){ - DOM.setStyleAttribute(this.getElement(), "cursor", value.getCssValue()); + if(styleClass == null){ + DOM.setStyleAttribute(this.getElement(), "cursor", value.getCssValue()); + } else { + // TODO: implement + } } } // sets the background-color style property of this element by using the GWT DOM class - public void setBackgroundColor(ColorValue value){ + public void setBackgroundColor(ColorValue value, String styleClass){ if(value != null){ - DOM.setStyleAttribute(this.getElement(), "backgroundColor", value.getCssValue()); + if(styleClass == null){ + DOM.setStyleAttribute(this.getElement(), "backgroundColor", value.getCssValue()); + } else { + // TODO: implement + } } } // sets the overflow style property of this element by using the GWT DOM class - public void setOverflow(Overflow value){ + public void setOverflow(Overflow value, String styleClass){ if(value != null){ - DOM.setStyleAttribute(this.getElement(), "overlof", value.getCssName()); + if(styleClass == null){ + DOM.setStyleAttribute(this.getElement(), "overlof", value.getCssName()); + } else { + // TODO: implement + } } } @@ -1434,45 +1594,49 @@ this.setZindex(this.getZindex()); this.setFloat(this.getFloat()); this.setClear(this.getClear()); - this.setVerticalAlign(this.getVerticalAlign(null)); - this.setMargin(this.getMargin(null)); - this.setMarginTop(this.getMarginTop(null)); - this.setMarginRight(this.getMarginRight(null)); - this.setMarginBottom(this.getMarginBottom(null)); - this.setMarginLeft(this.getMarginLeft(null)); - this.setBorderColor(this.getBorderColor(null)); - this.setBorderTopColor(this.getBorderTopColor(null)); - this.setBorderRightColor(this.getBorderRightColor(null)); - this.setBorderBottomColor(this.getBorderBottomColor(null)); - this.setBorderLeftColor(this.getBorderLeftColor(null)); - this.setBorderStyle(this.getBorderStyle(null)); - this.setBorderTopStyle(this.getBorderTopStyle(null)); - this.setBorderRightStyle(this.getBorderRightStyle(null)); - this.setBorderBottomStyle(this.getBorderBottomStyle(null)); - this.setBorderLeftStyle(this.getBorderLeftStyle(null)); - this.setBorderWidth(this.getBorderWidth(null)); - this.setBorderTopWidth(this.getBorderTopWidth(null)); - this.setBorderRightWidth(this.getBorderRightWidth(null)); - this.setBorderBottomWidth(this.getBorderBottomWidth(null)); - this.setBorderLeftWidth(this.getBorderLeftWidth(null)); - this.setBorderRadius(this.getBorderRadius(null)); - this.setBorderTopRightRadius(this.getBorderTopRightRadius(null)); - this.setBorderBottomRightRadius(this.getBorderBottomRightRadius(null)); - this.setBorderBottomLeftRadius(this.getBorderBottomLeftRadius(null)); - this.setBorderTopLeftRadius(this.getBorderTopLeftRadius(null)); - this.setPadding(this.getPadding(null)); - this.setPaddingTop(this.getPaddingTop(null)); - this.setPaddingRight(this.getPaddingRight(null)); - this.setPaddingBottom(this.getPaddingBottom(null)); - this.setPaddingLeft(this.getPaddingLeft(null)); - this.setWidth(this.getWidth(null)); - this.setMinWidth(this.getMinWidth(null)); - this.setMaxWidth(this.getMaxWidth(null)); - this.setHeight(this.getHeight(null)); - this.setMinHeight(this.getMinHeight(null)); - this.setMaxHeight(this.getMaxHeight(null)); - this.setCursor(this.getCursor(null)); - this.setBackgroundColor(this.getBackgroundColor(null)); - this.setOverflow(this.getOverflow(null)); + + String[] styleClasses = new String[]{null, GdlPsis.Scope.gdlActive, GdlPsis.Scope.gdlFocus, GdlPsis.Scope.gdlHover}; + for (String styleClass : styleClasses) { + this.setVerticalAlign(this.getVerticalAlign(styleClass), styleClass); + this.setMargin(this.getMargin(styleClass), styleClass); + this.setMarginTop(this.getMarginTop(styleClass), styleClass); + this.setMarginRight(this.getMarginRight(styleClass), styleClass); + this.setMarginBottom(this.getMarginBottom(styleClass), styleClass); + this.setMarginLeft(this.getMarginLeft(styleClass), styleClass); + this.setBorderColor(this.getBorderColor(styleClass), styleClass); + this.setBorderTopColor(this.getBorderTopColor(styleClass), styleClass); + this.setBorderRightColor(this.getBorderRightColor(styleClass), styleClass); + this.setBorderBottomColor(this.getBorderBottomColor(styleClass), styleClass); + this.setBorderLeftColor(this.getBorderLeftColor(styleClass), styleClass); + this.setBorderStyle(this.getBorderStyle(styleClass), styleClass); + this.setBorderTopStyle(this.getBorderTopStyle(styleClass), styleClass); + this.setBorderRightStyle(this.getBorderRightStyle(styleClass), styleClass); + this.setBorderBottomStyle(this.getBorderBottomStyle(styleClass), styleClass); + this.setBorderLeftStyle(this.getBorderLeftStyle(styleClass), styleClass); + this.setBorderWidth(this.getBorderWidth(styleClass), styleClass); + this.setBorderTopWidth(this.getBorderTopWidth(styleClass), styleClass); + this.setBorderRightWidth(this.getBorderRightWidth(styleClass), styleClass); + this.setBorderBottomWidth(this.getBorderBottomWidth(styleClass), styleClass); + this.setBorderLeftWidth(this.getBorderLeftWidth(styleClass), styleClass); + this.setBorderRadius(this.getBorderRadius(styleClass), styleClass); + this.setBorderTopRightRadius(this.getBorderTopRightRadius(styleClass), styleClass); + this.setBorderBottomRightRadius(this.getBorderBottomRightRadius(styleClass), styleClass); + this.setBorderBottomLeftRadius(this.getBorderBottomLeftRadius(styleClass), styleClass); + this.setBorderTopLeftRadius(this.getBorderTopLeftRadius(styleClass), styleClass); + this.setPadding(this.getPadding(styleClass), styleClass); + this.setPaddingTop(this.getPaddingTop(styleClass), styleClass); + this.setPaddingRight(this.getPaddingRight(styleClass), styleClass); + this.setPaddingBottom(this.getPaddingBottom(styleClass), styleClass); + this.setPaddingLeft(this.getPaddingLeft(styleClass), styleClass); + this.setWidth(this.getWidth(styleClass), styleClass); + this.setMinWidth(this.getMinWidth(styleClass), styleClass); + this.setMaxWidth(this.getMaxWidth(styleClass), styleClass); + this.setHeight(this.getHeight(styleClass), styleClass); + this.setMinHeight(this.getMinHeight(styleClass), styleClass); + this.setMaxHeight(this.getMaxHeight(styleClass), styleClass); + this.setCursor(this.getCursor(styleClass), styleClass); + this.setBackgroundColor(this.getBackgroundColor(styleClass), styleClass); + this.setOverflow(this.getOverflow(styleClass), styleClass); + } } }
-
lgiessmann＠common-lisp.net