Back to index

wims  3.65+svn20090927
BracketSymbol.java
Go to the documentation of this file.
00001 /*
00002 $Id: BracketSymbol.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.awt.image.ImageObserver;
00033 import fr.ove.openmath.jome.ctrlview.bidim.*;
00034 import fr.ove.openmath.jome.ctrlview.bidim.images.ImageLoader;
00035 
00036 
00043 public class BracketSymbol extends DisplayableImpl {
00051     private Image topInit;
00052     private Image middleInit;
00053     private Image bottomInit;
00054     
00058     private Image top;
00059     private Image middle;
00060     private Image bottom;
00061     
00065     private int heightExtremities;
00066     
00070     ImageObserver observer;
00071      
00079     public BracketSymbol(boolean isLeftBracket, int heightExtremities, ImageObserver observer) {
00080         if (isLeftBracket) {
00081             topInit = ImageLoader.getImage("LeftTopPar");
00082             middleInit = ImageLoader.getImage("LeftMiddlePar");
00083             bottomInit = ImageLoader.getImage("LeftBottomPar");
00084         }
00085         else {
00086             topInit = ImageLoader.getImage("RightTopPar");
00087             middleInit = ImageLoader.getImage("RightMiddlePar");
00088             bottomInit = ImageLoader.getImage("RightBottomPar");
00089         }
00090 
00091         this.heightExtremities = heightExtremities;
00092         this.observer = observer;
00093     }
00094     
00099     public void paint(Graphics g) {
00100         int height = getHeight();
00101         
00102         // On dessine la partie supérieure de la parenthèse
00103         g.drawImage(top, 0, 0, observer);
00104         
00105         // On dessine la partie centrale de la parenthèse
00106         for (int i = heightExtremities; i < height - heightExtremities; i += heightExtremities)
00107             g.drawImage(middle, 0, i, observer);
00108         
00109         // On dessine la partie inférieure de la parenthèse
00110         g.drawImage(bottom, 0, height - heightExtremities, observer);
00111     }
00112     
00116     public Dimension getPreferredSize() {
00117               MediaTracker tracker = new MediaTracker((Component) observer);
00118         // Le -1 signifie que la largeur sera proportionnelle à la hauteur.
00119         top = topInit.getScaledInstance(-1, heightExtremities, Image.SCALE_SMOOTH);
00120         tracker.addImage(top, 0);
00121         bottom = bottomInit.getScaledInstance(-1, heightExtremities, Image.SCALE_SMOOTH);
00122         tracker.addImage(bottom, 0);
00123         middle = middleInit.getScaledInstance(-1, heightExtremities, Image.SCALE_SMOOTH);
00124         tracker.addImage(middle, 0);
00125         
00126         // On attend que toutes les images soient chargées.
00127               try { tracker.waitForAll(); }
00128               catch (InterruptedException e) {
00129                   System.out.print(e.toString());
00130               }
00131               
00132               // Une fois que toutes les images ont été chargées, on les enlèves du media tracker.
00133         tracker.removeImage(top);
00134         tracker.removeImage(middle);
00135         tracker.removeImage(bottom);
00136 
00137         return new Dimension(top.getWidth(observer), getHeight());
00138     }
00139     
00144     public void setGraphicContext(GraphicContext graphicContext) {
00145         super.setGraphicContext(graphicContext);
00146         // Surcharge de cette méthode pour que l'on puisse récupérer en fonction du contexte graphique
00147         // du symbole, la hauteur des extrémité de la parenthèse.
00148         FontMetrics fm = Toolkit.getDefaultToolkit().getFontMetrics(graphicContext.getFont());
00149         heightExtremities = fm.getHeight() / 2;
00150     }
00151 }