Back to index

wims  3.65+svn20090927
RequestLayout.java
Go to the documentation of this file.
00001 /*
00002 $Id: RequestLayout.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.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 
00043 public class RequestLayout extends HorizontalLayout {
00047     private boolean insertSeparatorDisplay = true;
00048     
00055     private int prevNbComponent = 0;
00056     
00057     private String opeSymbol;
00058     
00059     private Display displaySlot = null;
00060     
00065     public void insertOperatorDisplay() {
00066         Display current, next;
00067         FormulaTreeStructure fatherFts = (FormulaTreeStructure) displayToLay.getListener();
00068         FormulaTreeStructure fts;
00069         StringDisplay stringDisplay;
00070         int nbComponent = displayToLay.getComponentCount();
00071         
00072         if (nbComponent > 1) {
00073             if (fatherFts.getResourceIdentifier().equals("request"))
00074                 opeSymbol = new String("  with  ");
00075             else
00076                 opeSymbol = new String("  if  ");
00077                 
00078             stringDisplay = new StringDisplay(displayToLay.getGraphicContext(), opeSymbol, true);
00079             stringDisplay.addControlListener(fatherFts);
00080             displayToLay.add(stringDisplay, stringDisplay, 1);
00081             nbComponent++;
00082         } 
00083         
00084         // Mise à jour du nombre de components présents dans le display.
00085         prevNbComponent = displayToLay.getComponentCount();
00086         // On n'a plus besoin d'insérer des displays d'opérateur.
00087         insertSeparatorDisplay = false;
00088         // On a rajouté un display, on demande le recalcul de tous les ancêtres
00089         // de l'instance.
00090         displayToLay.computeAncestorsAttributes();
00091     }
00092     
00096     public void validateSelection() {
00097     }
00098     
00103     public void validateDeselection(Display display) {
00104     }
00105     
00111     public Dimension computeAttributes() {
00112         int ascent = 0;
00113         int descent = 0;
00114         
00115         //Always add the container's insets!
00116         Insets insets = displayToLay.getParent().insets();
00117         int width = insets.left + insets.right;
00118         int height = insets.top + insets.bottom;
00119         
00120         Display tmp;
00121         
00122         int count = displayToLay.getComponentCount();
00123         Slot slot;
00124         Constant cte;
00125         int stop = 2;
00126         
00127         if (count == 1) {
00128             if (displaySlot != null) {
00129                 slot = (Slot) displaySlot.getListener();
00130                 if (slot.getChild(0) instanceof Constant) {
00131                     cte = (Constant) slot.getChild(0);
00132                     if (!cte.isTemplate()) {
00133                         displayToLay.add(displaySlot);
00134                         stop = 2;
00135                     }
00136                 }
00137                 else
00138                     stop = 1;
00139             }
00140         }
00141         else if (count == 2) {
00142             displaySlot = (Display) displayToLay.getComponent(1);
00143             slot = (Slot) displaySlot.getListener();
00144             if (slot.getChild(0) instanceof Constant) {
00145                 cte = (Constant) slot.getChild(0);
00146                 if (cte.isTemplate()) {
00147                     displayToLay.remove(displaySlot);
00148                     stop = 1;
00149                 }
00150             }
00151             else 
00152                 stop = 2;
00153         }
00154         
00155         
00156         // On regarde si le nombre de component dans le display a chnagé depuis
00157         // la dernière fois. Si oui, il faut contrôler s'il ne faut pas ajouter
00158         // des display d'opérateur.
00159         if (insertSeparatorDisplay || (prevNbComponent != ((Display) displayToLay).getComponentCount()))
00160             insertOperatorDisplay();
00161         
00162         updateLevel(displayToLay.getLevel());
00163         
00164         count = displayToLay.getComponentCount();
00165         stop = (count > 1) ? 2 : 1;
00166         
00167         // Ca va de la condition au with ou if selon le type
00168         for (int i = 0; i < stop; i++) {
00169             tmp = (Display) displayToLay.getComponent(i);
00170             tmp.setSize(tmp.getPreferredSize());
00171                     
00172             width += tmp.getWidth() + tmp.getShiftX();
00173                     
00174             ascent = Math.max(tmp.getAscent() - tmp.getShiftY(),
00175                               ascent);
00176                       
00177             descent = Math.max(tmp.getDescent() + tmp.getShiftY(),
00178                                descent);
00179                                 
00180         }
00181         
00182         
00183         if (count == 3) {
00184             tmp = (Display) displayToLay.getComponent(2);
00185             tmp.setSize(tmp.getPreferredSize());
00186             height = (int) Math.max(((Display) displayToLay.getComponent(0)).getHeight(), 
00187                                     ((Display) displayToLay.getComponent(2)).getHeight());
00188             width += tmp.getWidth() + tmp.getShiftX();
00189             displayToLay.setAscent(Math.max( ((Display) displayToLay.getComponent(0)).getAscent(), 
00190                                              ((Display) displayToLay.getComponent(2)).getAscent() ));
00191         }
00192         else {
00193             height = ((Display) displayToLay.getComponent(0)).getHeight();
00194             int shiftY = ((Display) displayToLay.getComponent(0)).getDescent();
00195             //count = displayToLay.getComponentCount();
00196             for (int i = 2; i < count; i++) {
00197                 tmp = (Display) displayToLay.getComponent(i);
00198                 tmp.setSize(tmp.getPreferredSize());
00199                 
00200                 if (i == 2) {
00201                     if (count > 3) {
00202                         // On fait en sorte que cet élément commence à 20 pixels du bord gauche du display le contenant
00203                         tmp.setShiftX(-width + 20 );
00204                         shiftY += tmp.getAscent()+ 10;
00205                         tmp.setShiftY(shiftY);
00206                     }
00207                     else
00208                         width += tmp.getWidth();
00209                 }
00210                 else {
00211                     tmp.setShiftX(-((Display) displayToLay.getComponent(i-1)).getWidth());
00212                     shiftY += ((Display) displayToLay.getComponent(i-1)).getDescent() + tmp.getAscent()+ 5;
00213                     tmp.setShiftY(shiftY);
00214                 }
00215                 
00216                 width = Math.max(width, 20 + tmp.getWidth());
00217                 
00218                 if (i == (count - 1))
00219                     height = shiftY + tmp.getHeight();
00220             }
00221             
00222             displayToLay.setAscent(Math.max( 0, ((Display) displayToLay.getComponent(0)).getAscent() ));
00223         }
00224         
00225         displayToLay.setSize(width , height);
00226         displayToLay.setDescent(height - displayToLay.getAscent());
00227         
00228         displayToLay.setComputeAttributes(false);
00229         
00230         return new Dimension(width, height);
00231     }
00232 
00233     /*
00234      * Lays out the container in the specified panel.
00235      * @param parent the component which needs to be laid out 
00236      */
00237      public void layoutContainer(Container parent) {
00238         // On regarde si le nombre de component dans le display a chnagé depuis
00239         // la dernière fois. Si oui, il faut contrôler s'il ne faut pas ajouter
00240         // des display d'opérateur.
00241         if (insertSeparatorDisplay || (prevNbComponent != ((Display) parent).getComponentCount()))
00242             insertOperatorDisplay();
00243         
00244         super.layoutContainer(parent);
00245     }
00246     
00247 
00251     public void rebuildDisplay() {
00252         Display tmp;
00253         int nbDisplay = ((FormulaTreeStructure) displayToLay.getListener()).getNbChildren();
00254         Display listDisplay[] = new Display[nbDisplay];
00255         
00256         for (int i = 0; i < displayToLay.getComponentCount(); i++) {
00257             tmp = (Display) displayToLay.getComponent(i);
00258             if (!tmp.isSymbolOperatorDisplay()) {
00259                 // A voir !!!!!
00260                 // Mais il semblerai que bon, sinon à la (re)construction du display il se base
00261                 // sur des anciennes valeurs, et donc pas tarrible niveau affichage.
00262                 tmp.setLocation(0, 0);
00263                 listDisplay[((FormulaTreeStructure) tmp.getListener()).getRank()] = tmp;
00264             }
00265         }
00266         
00267         // ATTENTION : ici, on enlève les displays fils de display, mais on ne les enlève pas de la liste
00268         // des listeners de la fts qu'il sont en train d'écouter. Exception faite pour les displays d'opérateur.
00269         displayToLay.removeAllDisplays();
00270         
00271         for (int i = 0; i < nbDisplay; i++)
00272             displayToLay.add(listDisplay[i]);
00273             
00274         // On a reconstruit le display, il faut maintenant insérer les displays d'opérateur.
00275         insertSeparatorDisplay = true;
00276     }
00277    
00278 }