// Copyright 1996, Marimba Inc. All Rights Reserved.


// @(#)PageWidget.java, 1.14, 09/20/96





package marimba.gui;





import java.awt.*;


import marimba.persist.*;





/**


 * This widget is a page in a folder.


 * It should not be used otherwise.


 *


 * @author	Arthur van Hoff


 * @version 	1.14, 09/20/96


 */


public class PageWidget extends GroupWidget {


    /**


     * The title of this page.


     * @see #getText


     * @see #setText


     */


    public String  title;





    /**


     * Get the properties.


     * @see #setProperties


     */


    public void getProperties(PropertyList list) {


	super.getProperties(list);


	list.setString("title", title, null);


    }





    /**


     * Set the properties.


     * @see #getProperties


     * @see #applyProperties


     */


    public void setProperties(PropertyList list) {


	super.setProperties(list);


	title = list.getString("title", null);


    }





    /**


     * Repaint the folder after the properties have


     * been applied, the tabs may have changed.


     * @see #setProperties


     */


    public void applyProperties(PropertyList list) {


	super.applyProperties(list);


	Widget parent = this.parent;


	if (parent != null) {


	    parent.repaint();


	}


    }





    /**


     * Get the title.


     * @see #title


     */


    public String getText() {


	return title;


    }





    /**


     * Set the title.


     * @see #title


     */


    public void setText(String str) {


	title = str;


	Widget parent = this.parent;


	if (parent != null) {


	    parent.repaint();


	}


    }





    /**


     * Send an event when this page becomes visible.


     */


    public void start() {


	postEvent(new Event(this, PAGE_EVENT, null));


    }


}