Back to index

wims  3.65+svn20090927
IntervalLayout.java
Go to the documentation of this file.
00001 /*
00002 $Id: IntervalLayout.java,v 1.3 2003/02/18 11:48:46 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.util.*;
00033 import fr.ove.openmath.jome.ctrlview.bidim.Display;
00034 import fr.ove.openmath.jome.ctrlview.bidim.DisplayLayout;
00035 import fr.ove.openmath.jome.ctrlview.bidim.selection.events.SelectionEvent;
00036 import fr.ove.openmath.jome.model.*;
00037 import fr.ove.utils.FontInfo;
00038 
00045 public class IntervalLayout extends EnclosingLayout {
00054     public void initDisplay(Display displayToLay) {
00055         super.initDisplay(displayToLay);  // Par cet appel, on ajoute dans displayToLay les crochets
00056         // On va maintenant y rajouter un display, dans lequel on va mettre les displays correspondants
00057         // aux bornes de l'intervalle, display à qui on va affecter un SeparatorOperatorLayout, qui va se charger
00058         // d'afficher entre chacun des éléments une virgule (un séparateur)
00059         Display boundsDisplay = new BidimDisplay(displayToLay.getGraphicContext());
00060         // On met un listener à boundsDisplay
00061         // En fait, il n'y en a pas besoin, dans le sens où il n'y a pas spécifiquement de fts qui
00062         // écoute le comportement de ce display. Néanmoins, il s'avère nécessaire qu'il en ait
00063         // un, par exemple lors de l'iconification, car c'est le display qui reçoit la demande
00064         // d'iconification qui envoie l'événement correspondant à la FTS. Or si ce display n'a pas
00065         // d'écouteur, alors pb. Par cohérence, l'écouteur du display d'opérateur, est le fts qui
00066         // représente cette opération. Par contre, la fts en question, n'écoute pas le display
00067         // d'opérateur.
00068         boundsDisplay.addControlListener((FormulaTreeStructure) displayToLay.getListener());
00069         
00070         SeparatorOperatorLayout layout = new SeparatorOperatorLayout();
00071         layout.initDisplay(boundsDisplay);
00072         boundsDisplay.setLayout(layout);
00073         
00074         // On l'ajoute comme fils à display
00075         this.displayToLay.add(boundsDisplay);
00076     }
00077     
00081     public SymbolDisplay createOpening() {
00082         // On récupère le fts associé (listener) au display.
00083         KaryOperator fts = (KaryOperator) displayToLay.getListener();
00084         
00085         SymbolDisplay bracket = new SymbolDisplay(displayToLay.getGraphicContext(), 
00086                                                   new SquaredBracketSymbol(fts.getTheOperator(), displayToLay));            
00087         // Le display de l'accolade est le display d'un opérateur (on peut le considérer comme tel)
00088         bracket.setIsSymbolOperatorDisplay(true);
00089         
00090         return bracket;
00091     }
00092     
00096     public SymbolDisplay createClosing() {
00097         // On récupère le fts associé (listener) au display.
00098         KaryOperator fts = (KaryOperator) displayToLay.getListener();
00099         
00100         SymbolDisplay bracket = new SymbolDisplay(displayToLay.getGraphicContext(), 
00101                                                   new SquaredBracketSymbol(fts.getEnding(), displayToLay));            
00102         // Le display de l'accolade est le display d'un opérateur (on peut le considérer comme tel)
00103         bracket.setIsSymbolOperatorDisplay(true);
00104         
00105         return bracket;
00106     }    
00107     
00113     public Dimension computeAttributes() {
00114         Display display = null;
00115         
00116         if (displayToLay.getComponentCount() > 3) {
00117             Display boundsDisplay = (Display) displayToLay.getComponent(2);
00118             Display d;
00119             for (int i = 3; i < displayToLay.getComponentCount(); ) {
00120                 d = (Display) displayToLay.getComponent(i);
00121                 // elementsDisplay.add(d) appelle un displayToLay.remove(d).
00122                 // remove(d), enlève également d de la liste des listeners de l'objet (fts) qu'il écoutait.
00123                 // Ce qu'on ne veut pas, puisqu'il s'agit d'un simple déplacement de display. 
00124                 d.setDoRemoveFromListListeners(false);
00125                 boundsDisplay.add(d);
00126                 // On remet le comportement de suppression par défault.
00127                 d.setDoRemoveFromListListeners(true);
00128             }
00129         }
00130         
00131         SymbolDisplay leftBracket = (SymbolDisplay) displayToLay.getComponent(0);
00132         SquaredBracketSymbol leftSymbol = (SquaredBracketSymbol) leftBracket.getSymbol();
00133         SymbolDisplay rightBracket = (SymbolDisplay) displayToLay.getComponent(1);
00134         SquaredBracketSymbol rightSymbol = (SquaredBracketSymbol) rightBracket.getSymbol();
00135         
00136         // On met la hauteur à 0, pour que dans tous les cas, le super.computeAttributes() ne soit pas
00137         // biaisée par une éventuelle nouvelle taille des éléments qui composent la liste.
00138         // Comme c'est plus loin qu'on leur fixe la taille....
00139         leftSymbol.setHeight(0);
00140         rightSymbol.setHeight(0);
00141         
00142         Dimension dim = super.computeAttributes();
00143         
00144         // Par contre, par rapport à comment est calculée la taille des accolades, dim comprend
00145         // déjà la taille des accolades
00146         int ascent = displayToLay.getAscent();
00147         int descent = displayToLay.getDescent();
00148         int height =  displayToLay.getHeight();
00149         int thickness = FontInfo.getLineThickness(displayToLay, displayToLay.getFont());
00150         
00151         leftSymbol.setAscent(ascent);
00152         leftSymbol.setDescent(descent);
00153         leftSymbol.setHeight(height);
00154         leftSymbol.setThickness(thickness);
00155         leftBracket.setComputeAttributes(true);
00156         leftBracket.invalidate();
00157         leftBracket.setSize(leftBracket.getPreferredSize());
00158 
00159         rightSymbol.setAscent(ascent);
00160         rightSymbol.setDescent(descent);
00161         rightSymbol.setHeight(height);
00162         rightSymbol.setThickness(thickness);
00163         rightBracket.setComputeAttributes(true);
00164         rightBracket.invalidate();
00165         rightBracket.setSize(rightBracket.getPreferredSize());
00166         
00167         // Cette taille là correspond au décalage qu'il faut appliquer à la dernière accolade
00168         rightBracket.setShiftX(dim.width - 2*rightBracket.getWidth());
00169         // Mais il faut l'enlever au premier terme de la liste qui doit être contre la première
00170         // accolade (because HonrizontalLayout)
00171         ((Display) displayToLay.getComponent(2)).setShiftX(-rightBracket.getShiftX() - rightBracket.getWidth());
00172         
00173         return dim;
00174     }
00175     
00179     public void rebuildDisplay() {
00180         // La taille des displays est probablement différente de ceux qui étaient
00181         // précédemment. On demande alors le recalcul des display ancêtres.
00182         displayToLay.computeAncestorsAttributes();
00183     }
00184    
00185 }