Back to index

wims  3.65+svn20090927
CurlySymbol.java
Go to the documentation of this file.
00001 /*
00002 $Id: CurlySymbol.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 CurlySymbol extends DisplayableImpl {
00051     private Image topInit;
00052     private Image middleInit;
00053     private Image bottomInit;
00054     private Image barInit;
00055     
00059     private Image top;
00060     private Image middle;
00061     private Image bottom;
00062     private Image bar;
00063     
00067     private int heightExtremities;
00068     
00072     ImageObserver observer;
00073      
00081     public CurlySymbol(boolean isLeftBracket, int heightExtremities, ImageObserver observer) {
00082         if (isLeftBracket) {
00083             topInit = ImageLoader.getImage("LeftTopCurl");
00084             middleInit = ImageLoader.getImage("LeftMiddleCurl");
00085             bottomInit = ImageLoader.getImage("LeftBottomCurl");
00086             barInit = ImageLoader.getImage("LeftBarCurl");
00087         }
00088         else {
00089             topInit = ImageLoader.getImage("RightTopCurl");
00090             middleInit = ImageLoader.getImage("RightMiddleCurl");
00091             bottomInit = ImageLoader.getImage("RightBottomCurl");
00092             barInit = ImageLoader.getImage("RightBarCurl");
00093         }
00094 
00095         this.heightExtremities = heightExtremities;
00096         this.observer = observer;
00097     }
00098     
00103     public void paint(Graphics g) {
00104         int height = getHeight();
00105         
00106         // On dessine la partie supérieure de l'accolade
00107         g.drawImage(top, 3, 0, observer);
00108         
00109         // On dessine les "barres", i.e. la partie que l'on va faire croitre pour ajuster correctement
00110         // la taille de l'accolade
00111         for (int i = heightExtremities; i < height - heightExtremities; i += heightExtremities)
00112             g.drawImage(bar, 3, i, observer);
00113         
00114         // On dessine la partie inférieure de l'accolade
00115         g.drawImage(bottom, 3, height - heightExtremities, observer);
00116         
00117         // On dessine la partie centrale de l'accolade
00118         // On essaie de faire en sorte que le milieu de l'accolade se trouve un peu au dessus de la baseline
00119         // Par exemple, aligné avec le +. La barre horizontale du + se trouve grosso modo à la moitié de
00120         // son ascent. Il se trouve que c'est la hauteur de middle.
00121         g.drawImage(middle, 3, getAscent() - middle.getHeight(observer), observer);
00122     }
00123     
00127     public Dimension getPreferredSize() {
00128               MediaTracker tracker = new MediaTracker((Component) observer);
00129               
00130               // La hauteur de la partie du milieu est égale à environ 2 fois les extrémités.
00131               
00132         // Le -1 signifie que la largeur sera proportionnelle à la hauteur.
00133         top = topInit.getScaledInstance(-1, heightExtremities, Image.SCALE_SMOOTH);
00134         tracker.addImage(top, 0);
00135         middle = middleInit.getScaledInstance(-1, heightExtremities*2, Image.SCALE_SMOOTH);
00136         tracker.addImage(middle, 0);
00137         bottom = bottomInit.getScaledInstance(-1, heightExtremities, Image.SCALE_SMOOTH);
00138         tracker.addImage(bottom, 0);
00139         bar = barInit.getScaledInstance(-1, heightExtremities, Image.SCALE_SMOOTH);
00140         tracker.addImage(bar, 0);
00141         
00142         // On attend que toutes les images soient chargées.
00143               try { tracker.waitForAll(); }
00144               catch (InterruptedException e) {
00145                   System.out.println(e.toString());
00146               }
00147               
00148         tracker.removeImage(top);
00149         tracker.removeImage(middle);
00150         tracker.removeImage(bottom);
00151         tracker.removeImage(bar);
00152 
00153         return new Dimension(top.getWidth(observer) + 6, getHeight());
00154     }
00155     
00164     public void setGraphicContext(GraphicContext graphicContext) {
00165         super.setGraphicContext(graphicContext);
00166         // Surcharge de cette méthode pour que l'on puisse récupérer en fonction du contexte graphique
00167         // du symbole, la hauteur des extrémité de l'accolade.
00168         FontMetrics fm = Toolkit.getDefaultToolkit().getFontMetrics(graphicContext.getFont());
00169         heightExtremities = fm.getHeight() / 4;
00170     }
00171 }