Back to index

wims  3.65+svn20090927
ConjugateLayout.java
Go to the documentation of this file.
00001 /*
00002 $Id: ConjugateLayout.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 fr.ove.openmath.jome.ctrlview.bidim.DisplayLayout;
00033 import fr.ove.openmath.jome.ctrlview.bidim.Display;
00034 import fr.ove.openmath.jome.ctrlview.bidim.Bar;
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 ConjugateLayout extends OverOperatorLayout {
00051     public Dimension computeAttributes() {
00052         SymbolDisplay displayBar = null;
00053         Bar bar = null;
00054         
00055         updateLevel(displayToLay.getLevel());
00056             
00057         // On est dans le cas particulier d'un symbol qui ne connais pas sa taille à l'avance.
00058         // Pour que cela puisse fonctionner correctement avec les autres displays, il faut qu'on
00059         // lui precise sa preferred size.
00060         // On met sa longueur à 0 pour éviter les élargissements infinis lors des différents retaillages
00061         // dus aux désiconifications.
00062         displayBar = (SymbolDisplay) displayToLay.getComponent(0);
00063         bar = (Bar) displayBar.getSymbol();
00064         bar.setWidth(0);
00065         bar.setHeight(FontInfo.getLineThickness(displayToLay, displayToLay.getFont())); // la hauteur fixe aussi ascent et descent        
00066         
00067         displayBar.setComputeAttributes(true);
00068         displayBar.setShiftY(2);
00069     
00070         // On calcule les attributs des display enfants comme si 
00071         // on avait affaire à un VerticalCenteredLayout
00072         Dimension dim = super.computeAttributes(); 
00073         
00074         // La différence réside en le calcul supplémentaire de la taille de la 
00075         // barre que l'on ne peut fixer après avoir calculé la largeur de l'argument
00076         bar.setWidth(dim.width + 2);
00077         displayBar.setSize(bar.getSize());
00078                                                 
00079         displayToLay.setAscent(((Display) displayToLay.getComponent(0)).getShiftY() +
00080                   ((Display) displayToLay.getComponent(0)).getHeight() + 
00081                   ((Display) displayToLay.getComponent(1)).getShiftY() +
00082                   ((Display) displayToLay.getComponent(1)).getAscent());
00083                   
00084         displayToLay.setDescent(displayToLay.getHeight() - displayToLay.getAscent());
00085         
00086         displayToLay.setSize(dim);
00087 
00088         displayToLay.setComputeAttributes(false);
00089         
00090         return dim;
00091     }
00092     
00096     public Display createOperatorDisplay() {
00097         SymbolDisplay bar = new SymbolDisplay(displayToLay.getGraphicContext(), new Bar());
00098         // Le display de la barre est le display d'un opérateur (on peut le considérer comme tel)
00099         bar.setIsSymbolOperatorDisplay(true);
00100         
00101         return bar;
00102     }
00103 }