Back to index

wims  3.65+svn20090927
ScriptLayout.java
Go to the documentation of this file.
00001 /*
00002 $Id: ScriptLayout.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 fr.ove.openmath.jome.ctrlview.bidim.Display;
00033 import fr.ove.openmath.jome.ctrlview.bidim.DisplayLayout;
00034 import fr.ove.openmath.jome.ctrlview.bidim.HorizontalLayout;
00035 import fr.ove.openmath.jome.ctrlview.bidim.selection.events.SelectionEvent;
00036 import fr.ove.openmath.jome.model.*;
00037 
00046 public abstract class ScriptLayout extends HorizontalLayout {
00051     public void updateLevel(int level) {
00052         Display tmp;
00053         
00054         // Pour éviter de refaire le calcul plusieurs fois....
00055         if (displayToLay.getUpdateLevel()) {
00056             // On met le niveau adéquat
00057             displayToLay.setLevel(level);
00058             // On scale le display en fonction du niveau
00059             displayToLay.scaleDisplay();
00060             // On n'a plus besoin de mettre à jour le niveau de l'instance
00061             displayToLay.setUpdateLevel(false);
00062             
00063             // Le premier display fils possède le même niveau que son père.
00064             tmp = (Display) displayToLay.getComponent(0);
00065             ((DisplayLayout) tmp.getLayout()).updateLevel(level);
00066             
00067             // Le deuxième display fils possède le même niveau que la base + 1.
00068             // (on applique une réduction de taille)
00069             tmp = (Display) displayToLay.getComponent(1);
00070             ((DisplayLayout) tmp.getLayout()).updateLevel(level+1);
00071         }
00072     }
00073     
00077     public void validateSelection() {
00078         SelectionEvent selEvt = new SelectionEvent(displayToLay);
00079 
00080         // La validité de la sélection est triviale.
00081         // Si un des éléments de la puissance est sélectionné, alors la sélection
00082         // de l'autre élément entraîne la sélection de toute la puissance.
00083         Display base = (Display) displayToLay.getComponent(0);
00084         Display script = (Display) displayToLay.getComponent(1);
00085         if (base.gotSelectedElements() && script.gotSelectedElements()) {
00086             displayToLay.select();
00087             // On purge la liste des éléments sélectionnés.
00088             selEvt.setAction(SelectionEvent.PURGE, null);
00089             displayToLay.fireSelectionEvent(selEvt);
00090             // On y ajoute notre puissance.
00091             selEvt.setAction(SelectionEvent.ADD, displayToLay);
00092             displayToLay.fireSelectionEvent(selEvt);
00093         }
00094         
00095         // On a vérifié la validité de la sélection de la puissance. On doit maitenant
00096         // la contrôler au niveau supérieur, au niveau du père.
00097         // Ex : on a l'expression A+B^C et on a A déjà sélectionné. On sélectionne C.
00098         // D'un pt de vue sémantique (oui, on va dire ça comme ça) A et C ne peuvent
00099         // être sélectionnés séparément. Tout doit être sélectionné. Et ça, c'est la 
00100         // validation de la sélection qui va le déterminer. oufff....
00101         Display display = displayToLay;
00102         if (displayToLay.getParent() instanceof Display) {
00103             display = (Display) displayToLay.getParent();
00104             FormulaTreeStructure fts = (FormulaTreeStructure) display.getListener();
00105             if (fts.getFather() != null) // Si fts n'est pas la racine de la formule, on valide la sélection
00106                 ((DisplayLayout) display.getLayout()).validateSelection();
00107         }
00108 
00109         // On met à jour l'affichage.
00110         display.repaint();
00111     }
00112     
00117     public void validateDeselection(Display display) {
00118         Display tmp;
00119         SelectionEvent selEvt = new SelectionEvent(displayToLay);
00120         
00121         if (displayToLay.isSelected()) {
00122             // On désélectionne la puissance
00123             displayToLay.setNotSelected();
00124             // On enlève le display père de la liste des display sélectionnés.
00125             selEvt.setAction(SelectionEvent.REMOVE, displayToLay);
00126             displayToLay.fireSelectionEvent(selEvt);
00127             
00128             // Si la puissance toute entière était sélectionnée, donc présente dans la liste
00129             // des éléments sélectionné. Ce n'est pas le cas de la base et de l'exposant.
00130             // Donc en fonction de cela, il faut y ajouter l'élément adéquat
00131             if (((Display) displayToLay.getComponent(0)).isSelected())
00132                 // On a demandé la désélection en cliquant sur l'exposant, ce qui revient
00133                 // à sélectionner uniquement la base.
00134                 // On l'ajoute donc dans la liste des display sélectionnés.
00135                 selEvt.setAction(SelectionEvent.ADD, (Display) displayToLay.getComponent(0));
00136             else
00137                 // On a demandé la désélection en cliquant sur la base, ce qui revient
00138                 // à sélectionner uniquement l'exposant.
00139                 // On l'ajoute donc dans la liste des display sélectionnés.
00140                 selEvt.setAction(SelectionEvent.ADD, (Display) displayToLay.getComponent(1));
00141 
00142             displayToLay.fireSelectionEvent(selEvt);
00143 
00144             // Comme pour la sélection, on contrôle la validité de la désélection.
00145             Display father = displayToLay;
00146             if (displayToLay.getParent() instanceof Display) {
00147                 father = (Display) displayToLay.getParent();
00148                 FormulaTreeStructure fts = (FormulaTreeStructure) father.getListener();
00149                 if (fts.getFather() != null)
00150                     ((DisplayLayout) father.getLayout()).validateDeselection(displayToLay);
00151             }
00152             // Hé oui, on contrôle la validité de la sélection... dans une désélection.
00153             // Toujours le même pb, est-ce que le nouvel état de la sélection (après
00154             // désélection donc) est syntaxiquement cohérent ?
00155             validateSelection();
00156             
00157             // On met à jour l'affichage.
00158             father.repaint();
00159         }        
00160     }
00161     
00165     public void rebuildDisplay() {
00166         Display tmp;
00167         Display base = null;
00168         Display script = null;
00169         // On parcourre la liste des displays pour trouver qui est qui.
00170         for (int i = 0; i < 2; i++) {
00171             tmp = (Display) displayToLay.getComponent(i);
00172             // On fait les initialisations qui s'imposent pour le bon repositionnement de chacun.
00173             tmp.setLocation(0,0);
00174             if (((FormulaTreeStructure) tmp.getListener()).getRank() == 0)
00175                 base = tmp;
00176             else 
00177                 script = tmp;
00178         }
00179         // On a retrouvé qui est qui, on reconstruit le display pour tout mettre
00180         // à la bonne position.
00181         displayToLay.removeAllDisplays();
00182         displayToLay.add(base);
00183         displayToLay.add(script);
00184         // La taille des displays est probablement différente de ceux qui étaient
00185         // précédemment. On demande alors le recalcul des display ancêtres.
00186         displayToLay.computeAncestorsAttributes();
00187     }
00188 }