Back to index

wims  3.65+svn20090927
StringDisplay.java
Go to the documentation of this file.
00001 /*
00002 $Id: StringDisplay.java,v 1.3 2003/02/18 11:48:47 sander Exp $
00003 */
00004 
00005 
00006 /*
00007 Copyright (C) 2001-2002 Mainline Project (I3S - ESSI - CNRS -UNSA)
00008 
00009 This library is free software; you can redistribute it and/or
00010 modify it under the terms of the GNU Lesser General Public
00011 License as published by the Free Software Foundation; either
00012 version 2.1 of the License, or (at your option) any later version.
00013 
00014 This library is distributed in the hope that it will be useful,
00015 but WITHOUT ANY WARRANTY; without even the implied warranty of
00016 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
00017 Lesser General Public License for more details.
00018 
00019 You should have received a copy of the GNU Lesser General Public
00020 License along with this library; if not, write to the Free Software
00021 Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
00022 
00023 For further information on the GNU Lesser General Public License,
00024 see: http://www.gnu.org/copyleft/lesser.html
00025 For further information on this library, contact: mainline@essi.fr
00026 */
00027 
00028 
00029 package fr.ove.openmath.jome.ctrlview.bidim;
00030 
00031 import java.awt.*;
00032 import java.awt.event.*;
00033 import java.text.*;
00034 import fr.ove.utils.NumberUtils;
00035 import fr.ove.openmath.jome.ctrlview.bidim.StringLayout;
00036 import fr.ove.openmath.jome.ctrlview.bidim.Display;
00037 import fr.ove.openmath.jome.ctrlview.bidim.GraphicContext;
00038 import fr.ove.openmath.jome.model.*;
00039 import fr.ove.openmath.jome.model.events.ModelEvent;
00040 
00047 public class StringDisplay extends AbstractStringDisplay {
00055     public StringDisplay(GraphicContext graphicContext, String string, boolean isSymbolOperatorDisplay ) {
00056         super(graphicContext, string);
00057         setIsSymbolOperatorDisplay(isSymbolOperatorDisplay);
00058         StringLayout layout = new StringLayout();
00059         layout.initDisplay(this);
00060         setLayout(layout);
00061         
00062         addMouseListener(
00063             new MouseAdapter() {
00064                 public void mouseEntered(MouseEvent e) {
00065                     if (!isSymbolOperatorDisplay()) {
00066                         if (getListener() instanceof VariableOrNumber) {
00067                             VariableOrNumber listener = (VariableOrNumber) getListener();
00068                             if (listener.isNumber() && !listener.isInteger()) {
00069                                 // On a affaire à un float
00070                                 String value = listener.getValue();
00071                                 
00072                                 //if (!value.equals(StringDisplay.this.getString())) {
00073                                 if (!value.equals(getString())) {
00074                                     setString(value);
00075                                     invalidate();
00076                                     computeAncestorsAttributes();
00077                                     Container container = StringDisplay.this;
00078                                     while (container.getParent() != null)
00079                                         container = container.getParent();
00080                                         
00081                                     container.validate();
00082                                     container.repaint();
00083                                 }
00084                             }
00085                         }
00086                     }
00087                 }
00088                 
00089                 public void mouseExited(MouseEvent e) {
00090                     if (!isSymbolOperatorDisplay()) {
00091                         if (getListener() instanceof VariableOrNumber) {
00092                             VariableOrNumber listener = (VariableOrNumber) getListener();
00093                             if (listener.isNumber() && !listener.isInteger()) {
00094                                 // On a affaire à un float
00095                                 String value = listener.getValue();
00096                                 String newString = NumberUtils.formatDouble(value);
00097                                 
00098                                 if (!newString.equals(value)) {
00099                                     setString(newString);
00100                                     StringDisplay.this.invalidate();
00101                                     StringDisplay.this.computeAncestorsAttributes();
00102                                     Container container = StringDisplay.this;
00103                                     while (container.getParent() != null)
00104                                         container = container.getParent();
00105                                         
00106                                     container.validate();
00107                                     container.repaint();
00108                                 }
00109                             }
00110                         }
00111                     }
00112                 }
00113             }
00114         );
00115     }
00116     
00121     public void consumeModelEvent(ModelEvent modelEvent) {
00122         // En principe, c'est le seul événement que doit recevoir ce type de display
00123         // De plus, forcément, le display représenté n'est pas le display d'un opérateur.
00124         switch (modelEvent.getAction()) {
00125             case ModelEvent.UPDATE :
00126                 //System.out.println("ModelEvent.UPDATE : on update le StringDisplay");
00127                 VariableOrNumber src = (VariableOrNumber) modelEvent.getSource();
00128                 
00129                 // On met à jour le display.
00130                 // Ca c'est pour la troncature de l'affichage d'une nombre flottant dépassant
00131                 // 2 chiffres après la virgule
00132                 if (!isSymbolOperatorDisplay()) {
00133                     if (src.isNumber() && !src.isInteger())
00134                         // On a affaire à un float
00135                         setString(NumberUtils.formatDouble(src.getValue()));
00136                     else
00137                         setString(src.getValue());
00138                 }
00139                 else
00140                     setString(src.getValue());
00141 
00142                 computeAncestorsAttributes();
00143                 invalidate();
00144         }
00145     }
00146 }