//****************************************************************************
// CLASS NAME:	ReachabilityDisplayPanel.java
//
// AUTHOR:	Rick Brink
//		    rick@mail.csh.rit.edu
//		    http://www.csh.rit.edu/~rick
//
// VERSION:	1.0
//
// HISTORY:	4/16/96		Initial Version
//
// COPYRIGHT INFORMATION:
//
// This program and the Java source is in the public domain.
// Permission to use, copy, modify, and distribute this software
// and its documentation for NON-COMMERCIAL purposes and
// without fee is hereby granted.
//
//    Copyright 1996
//
//    Rick Brink
//    1266 Brighton-Henrietta Townline Rd.
//    Rochester, NY 14623
//
// DISCLAIMER:
//
// The author claims no responsibility for any damage, direct or indirect,
// to any harware or software as a result of using this program.
//****************************************************************************

import java.lang.Thread;
import java.util.Vector;
import java.awt.TextArea;
import java.awt.Frame;
import java.awt.Font;
import java.awt.FontMetrics;
import java.awt.Button;
import java.awt.Event;
import java.awt.Toolkit;
import java.awt.Color;
import java.awt.Panel;
import java.awt.Label;
import java.awt.Scrollbar;
import java.awt.Graphics;
import java.awt.BorderLayout;
import java.awt.Dimension;

/**
  * A class to display a Petri Net Reachability Tree in a Panel
  *
  * @see java.lang.Thread
  * @see java.util.Vector
  * @see java.awt.TextArea
  * @see java.awt.Frame
  * @see java.awt.Font
  * @see java.awt.FontMetrics
  * @see java.awt.Button
  * @see java.awt.Event
  * @see java.awt.Toolkit
  * @see java.awt.Color
  * @see java.awt.Panel
  * @see java.awt.Label
  * @see java.awt.Scrollbar
  * @see java.awt.Graphics
  * @see java.awt.BorderLayout
  * @see java.awt.Dimension
  *
  * @version 1.0 July 3, 1996
  *
  * @author  Rick Brink
**/
class ReachabilityDisplayPanel extends Panel {
    /** Holds Vectors of nodes of the reachability tree **/
    private protected Vector treeVector_;

    /** Vector holding the data for a single node of the tree **/
    private protected Vector nodeVector_;

    /** String to hold a single marking **/
    private protected String markingString_;

    /** String to hold a transition label **/
    private protected String transitionString_;

    /** Number of spaces to indent a node of the tree **/
    private protected int indentChars_;

    /** Width of the initial marking of a node in the tree **/
    private protected int width_;

    /** Controls horizontal scrolling of the DesignPanel **/
    private protected Scrollbar horizontalScrollbar_;

    /** Controls vertical scrolling of the DesignPanel **/
    private protected Scrollbar verticalScrollbar_;

    /** Indicates if searchText_ items should be highlighted **/
    private protected boolean search_;

    /** Marking to be highlighted if in tree and search_ is true **/
    private protected String searchText_;

    /** searchText_ with an '*' on the end, to detect final markings **/
    private protected String searchTextAsterick_;

    /** X offset used for scrollbar **/
    private protected int xOffset_;

    /** Y offset used for scrollbar **/
    private protected int yOffset_;

    /** Width of the Panel **/
    private protected int panelWidth_;

    /** Height of the Panel **/
    private protected int panelHeight_;

    /** Number of lines in the Reachability tree **/
    private protected int lines_;

    /** Number of pixels to move down after each line in the tree **/
    private protected int yIncrement_;

    /**
      * Construct a new Reachability Tree Panel, add scrollbars, and paint
    **/
    public ReachabilityDisplayPanel(Vector treeVector, boolean search,
                                    String searchText) {
        treeVector_ = treeVector;
        search_ = search;
        searchText_ = searchText;
        searchTextAsterick_ = searchText_.concat("*");
        lines_ = 0;
        repaint();
        setLayout(new BorderLayout());

        // Add scrollbars
        verticalScrollbar_ = new Scrollbar(Scrollbar.VERTICAL);
        add("East", verticalScrollbar_);
        horizontalScrollbar_ = new Scrollbar(Scrollbar.HORIZONTAL);
        add( "South", horizontalScrollbar_);
    }


    /**
      * The paint method is the main method for displaying the
      * reachability tree.  This method also will highlight searchText_
      * if search_ is true.
    **/
    public void paint (Graphics g) {
        String tempString__ = "";
        int yPos__;
        int xPos__;
        Label label__;
        Font treeFont__ = new Font("Dialog", Font.PLAIN, 12);
        g.setFont(treeFont__);

        // Get FontMetrics
        Toolkit toolkit_ = Toolkit.getDefaultToolkit();
        FontMetrics fm__ = toolkit_.getFontMetrics(treeFont__);
        yIncrement_ = fm__.getHeight();
        yPos__ = yIncrement_;
        xPos__ = 0;

        for (int i__ = 0; i__ < treeVector_.size(); i__++) {
            nodeVector_ = (Vector) treeVector_.elementAt(i__);
            markingString_ = (String) nodeVector_.elementAt(0);
            width_ = fm__.stringWidth(markingString_);

            // If this is a search display and markingString_
            // matches the searchText_, use red color to display
            if (search_) {
                if ((searchText_.equals(markingString_)) ||
                   (searchTextAsterick_.equals(markingString_))) {
                        g.setColor(Color.red);
                }
            }

            g.drawString(markingString_, xPos__ - xOffset_, yPos__ - yOffset_);
            xPos__ = xPos__ + fm__.stringWidth(markingString_);
            g.setColor(Color.black);

            for (int j__ = 1; j__ < nodeVector_.size() - 1; j__ = j__+2) {
                transitionString_ = (String) nodeVector_.elementAt(j__);
                markingString_ = (String) nodeVector_.elementAt(j__+1);
                tempString__ = new String("-" + transitionString_ + "->");
                g.drawString(tempString__, xPos__ - xOffset_, yPos__ - yOffset_);
                xPos__ = xPos__ + fm__.stringWidth(tempString__);

                // If this is a search display and markingString_
                // matches the searchText_, use red color to display
                if (search_) {
                    if ((searchText_.equals(markingString_)) ||
                       (searchTextAsterick_.equals(markingString_))) {
                            g.setColor(Color.red);
                    }
                }

                g.drawString(markingString_, xPos__ - xOffset_, yPos__ - yOffset_);
                g.setColor(Color.black);
                xPos__ = width_;
                yPos__ = yPos__ + yIncrement_;
                lines_++;
            }

            xPos__ = 0;
            yPos__ = yPos__ + yIncrement_;
            lines_++;
        }
    }

    /**
      * Used for setting offsets when SCROLL events occur so
      * scrollbars can be set to view the appropriate areas
      * of the Panel
    **/
    public boolean handleEvent(Event e) {
        if (e.target == horizontalScrollbar_) {
            switch (e.id) {
                case Event.SCROLL_LINE_UP:
                case Event.SCROLL_LINE_DOWN:
                case Event.SCROLL_PAGE_UP:
                case Event.SCROLL_PAGE_DOWN:
                case Event.SCROLL_ABSOLUTE:
                    xOffset_ = ((Integer)e.arg).intValue();
                    break;
            }
            repaint();
            return (true);
        }
        else if (e.target == verticalScrollbar_) {
            switch (e.id) {
                case Event.SCROLL_LINE_UP:
                case Event.SCROLL_LINE_DOWN:
                case Event.SCROLL_PAGE_UP:
                case Event.SCROLL_PAGE_DOWN:
                case Event.SCROLL_ABSOLUTE:
                    yOffset_ = ((Integer)e.arg).intValue();
                    break;
            }
            repaint();
            return (true);
        }
        return (super.handleEvent(e));

    }

    /**
      * Called when the Window size changes so that the
      * scrollabrs may be updated appropriately.
    **/
    public synchronized void reshape(int x, int y, int width, int height) {
        super.reshape(x, y, width, height);

        Dimension hbarSize__ = horizontalScrollbar_.size();
        Dimension vbarSize__ = verticalScrollbar_.size();
        panelWidth_ = width - vbarSize__.width;
        panelHeight_ = height - hbarSize__.height;
        horizontalScrollbar_.setValues(xOffset_, panelWidth_, 0,
            1000 - panelWidth_);
        verticalScrollbar_.setValues(yOffset_, panelHeight_, 0,
            lines_*yIncrement_);
        horizontalScrollbar_.setPageIncrement(panelWidth_/2);
        verticalScrollbar_.setPageIncrement(panelHeight_/2);
        repaint();
    }

}
