Back to index

wims  3.65+svn20090927
MapsArrayLayout.java
Go to the documentation of this file.
00001 /*
00002 $Id: MapsArrayLayout.java,v 1.3 2003/02/18 11:48:46 sander Exp $
00003 modified MapsToSigmaLayout.java
00004 */
00005 
00006 
00007 /*
00008 Copyright (C) 2001-2002 Mainline Project (I3S - ESSI - CNRS -UNSA)
00009 
00010 This library is free software; you can redistribute it and/or
00011 modify it under the terms of the GNU Lesser General Public
00012 License as published by the Free Software Foundation; either
00013 version 2.1 of the License, or (at your option) any later version.
00014 
00015 This library is distributed in the hope that it will be useful,
00016 but WITHOUT ANY WARRANTY; without even the implied warranty of
00017 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
00018 Lesser General Public License for more details.
00019 
00020 You should have received a copy of the GNU Lesser General Public
00021 License along with this library; if not, write to the Free Software
00022 Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
00023 
00024 For further information on the GNU Lesser General Public License,
00025 see: http://www.gnu.org/copyleft/lesser.html
00026 For further information on this library, contact: mainline@essi.fr
00027 */
00028 
00029 
00030 package fr.ove.openmath.jome.ctrlview.bidim;
00031 
00032 import java.awt.*;
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.HorizontalLayout;
00036 import fr.ove.openmath.jome.ctrlview.bidim.selection.events.SelectionEvent;
00037 import fr.ove.openmath.jome.model.*;
00038 
00054 public abstract class MapsArrayLayout extends HorizontalLayout  implements OperatorDisplayCreator {
00063     public void initDisplay(Display displayToLay) {
00064         super.initDisplay(displayToLay);
00065         
00066         Display array = createOperatorDisplay();
00067         array.addControlListener(this.displayToLay.getListener());
00068         this.displayToLay.add(array);
00069     }
00070     
00075     public void updateLevel(int level) {
00076         Display tmp;
00077         
00078         if (displayToLay.getUpdateLevel()) {            
00079             displayToLay.updateChildrenLevel();
00080             
00081             // On met à jour le niveau du display géré par le LM.
00082             displayToLay.setLevel(level);
00083             displayToLay.setUpdateLevel(false);
00084             
00085             // Le symbole a le même niveau que le display
00086             tmp = (Display) displayToLay.getComponent(0);
00087             ((DisplayLayout) tmp.getLayout()).updateLevel(level);
00088             tmp.setUpdateLevel(false);
00089             int count = displayToLay.getComponentCount();
00090             if (count > 1) {
00091                 // La borne inférieure a le niveau du dispay +1
00092                 tmp = (Display) displayToLay.getComponent(1);
00093                 ((DisplayLayout) tmp.getLayout()).updateLevel(level+1);
00094                 tmp.setUpdateLevel(false);
00095                 if (count > 2) {
00096                     // La borne supérieure a le niveau du dispay +1
00097                     tmp = (Display) displayToLay.getComponent(2);
00098                     ((DisplayLayout) tmp.getLayout()).updateLevel(level+1);
00099                     tmp.setUpdateLevel(false);
00100                 }
00101             }
00102         }
00103     }
00104 
00109     public void validateSelection() {
00110         Display symbol = (Display) displayToLay.getComponent(0);
00111         //Display expression = (Display) displayToLay.getComponent(1);
00112         //symbool=0 onder=1 boven=2
00113         int count = displayToLay.getComponentCount();
00114         
00115         // Si le symbole est sélectionné, on sélectionne tout le display
00116         if (symbol.isSelected())
00117             displayToLay.select();
00118         else if (count > 1) {
00119             Display lower = (Display) displayToLay.getComponent(1);
00120             Display upper;
00121             
00122             if (lower.gotSelectedElements()) {
00123                 if (count > 2) {
00124                     upper = (Display) displayToLay.getComponent(2);
00125                     if (upper.gotSelectedElements())
00126                         displayToLay.select();
00127                 }
00128             }
00129         }
00130         
00131         // Quand on est ici, si display est sélectionné, alors c'est qu'on a validé un des tests
00132         // ci-dessus. On doit alors mettre à jour le gestionnaire de sélections, et y ajouter display
00133         if (displayToLay.isSelected()) {
00134             SelectionEvent selEvt = new SelectionEvent(displayToLay);
00135             // On purge la liste des éléments sélectionnés.
00136             selEvt.setAction(SelectionEvent.PURGE, null);
00137             displayToLay.fireSelectionEvent(selEvt);
00138             // On y ajoute notre puissance.
00139             selEvt.setAction(SelectionEvent.ADD, displayToLay);
00140             displayToLay.fireSelectionEvent(selEvt);
00141         }
00142 
00143         // On a vérifié la validité de la sélection de la puissance. On doit maitenant
00144         // la contrôler au niveau supérieur, au niveau du père.
00145         Display display = displayToLay;
00146         if (display.getParent() instanceof Display) {
00147             display = (Display) display.getParent();
00148             //if (!(display.getListener() instanceof Formula))
00149             FormulaTreeStructure fts = (FormulaTreeStructure) display.getListener();
00150             if (fts.getFather() != null)
00151                 ((DisplayLayout) display.getLayout()).validateSelection();
00152         }
00153 
00154         // On met à jour l'affichage.
00155         display.repaint();
00156     }
00157     
00162     public void validateDeselection(Display display) {
00163         Display father = displayToLay;
00164         SelectionEvent selEvt = new SelectionEvent(father);
00165         
00166         if (father.isSelected()) {
00167             father.setNotSelected();
00168             // On enlève le display père de la liste des display sélectionnés.
00169             selEvt.setAction(SelectionEvent.REMOVE, father);
00170             father.fireSelectionEvent(selEvt);
00171             int count = father.getComponentCount();
00172             ((Display) father.getComponent(0)).setNotSelected();// On désélectionne le symbole.
00173             if (count > 1) {
00174                 ((Display) father.getComponent(1)).deselect();// On désélectionne la borne inf.
00175                 if (count > 2) 
00176                     ((Display) father.getComponent(2)).deselect();// On désélectionne la borne sup.
00177             }
00178             
00179             // Comme pour la sélection, on contrôle la validité de la désélection.
00180             if (father.getParent() instanceof Display) {
00181                 father = (Display) father.getParent();
00182                 FormulaTreeStructure fts = (FormulaTreeStructure) father.getListener();
00183                 if (fts.getFather() != null)
00184                     ((DisplayLayout) father.getLayout()).validateDeselection(displayToLay);
00185             }
00186             // Hé oui, on contrôle la validité de la sélection... dans une désélection.
00187             // Toujours le même pb, est-ce que le nouvel état de la sélection (après
00188             // désélection donc) est syntaxiquement cohérent ?
00189             validateSelection();
00190             
00191             // On met à jour l'affichage.
00192             father.repaint();
00193         }        
00194     }
00195 
00201     public Dimension computeAttributes() {
00202         int ascent = 0;
00203         int descent = 0;
00204 
00205         updateLevel(displayToLay.getLevel());
00206 
00207         int width = 0;
00208         int height = 0;
00209         
00210         Display symbol, lower, upper;
00211         int gap = 0;
00212         
00213         // On calcule la taille du symbole
00214         symbol = (Display) displayToLay.getComponent(0);
00215         symbol.setSize(symbol.getPreferredSize());
00216         
00217         int width1 = symbol.getWidth();
00218         int count = displayToLay.getComponentCount();
00219         if (count > 1) {
00220             // On calcule la taille de la borne inférieure
00221             lower = (Display) displayToLay.getComponent(1);
00222             lower.setSize(lower.getPreferredSize());
00223             lower.setShiftY(symbol.getDescent() + lower.getAscent() + gap);
00224             
00225             width1 = Math.max(lower.getWidth(), width1);
00226             
00227             if (count > 2 ) {
00228                 // On calcule la taille de la borne supérieure
00229                 upper = (Display) displayToLay.getComponent(2);
00230                 upper.setSize(upper.getPreferredSize());
00231                 width1 = Math.max(upper.getWidth(), width1);
00232                 upper.setShiftX(-(lower.getWidth() + upper.getWidth()) / 2);
00233                 upper.setShiftY(-(symbol.getAscent() + upper.getDescent() + gap));
00234                 ascent = symbol.getAscent() + upper.getHeight() + gap;
00235             }
00236             else {
00237                 ascent = symbol.getAscent();
00238             }
00239             
00240             symbol.setShiftX((width1 - symbol.getWidth()) / 2);
00241             lower.setShiftX(-(symbol.getWidth() + lower.getWidth())/2 );
00242             descent = symbol.getDescent() + lower.getHeight() + gap;
00243         }
00244         else {
00245             ascent = symbol.getAscent();
00246             descent = symbol.getDescent();
00247         }
00248                 
00249         displayToLay.setAscent(ascent);
00250         displayToLay.setDescent(descent);
00251         
00252         width += width1 + 4*gap; // 1 gap entre symbole et expression, et 3 après expression  
00253         
00254         height += ascent + descent;
00255         displayToLay.setSize(width , height);
00256         
00257         displayToLay.setComputeAttributes(false);
00258         return new Dimension(width, height);
00259     }
00260     
00264     public void rebuildDisplay() {
00265         
00266         //Faudra faire ce qui faut !!!!
00267         
00268         // La taille des displays est probablement différente de ceux qui étaient
00269         // précédemment. On demande alors le recalcul des display ancêtres.
00270         displayToLay.computeAncestorsAttributes();
00271     }
00272    
00273 }