animationhistory.java

Petri网分析工具PIPE is open-source

package pipe.gui;

import java.awt.Color;
import java.util.Enumeration;
import java.util.Vector;

import javax.swing.JTextPane;
import javax.swing.text.BadLocationException;
import javax.swing.text.Document;
import javax.swing.text.Style;
import javax.swing.text.StyleConstants;
import javax.swing.text.StyleContext;


/** Class to represent the history of the net animation */
public class AnimationHistory extends JTextPane {

  /** Holds all the transitions in the sequence */
  public Vector fSeq;
  private String initText;
  private Document doc;
  private Style emph;
  private Style bold;
  private Style regular;
  private int currentItem;


  public AnimationHistory(String text) throws javax.swing.text.BadLocationException {
    super();
    initText= text;
    initStyles();
    doc = getDocument();
    doc.insertString(doc.getLength(),text,bold);
    fSeq = new Vector();
    currentItem = 1;

  }

  private void initStyles() {
    Style def = StyleContext.getDefaultStyleContext().getStyle(StyleContext.DEFAULT_STYLE);
    regular = addStyle("regular", def);
    StyleConstants.setFontFamily(def, "SansSerif");

    emph = addStyle("currentTransition",regular);
    StyleConstants.setBackground(emph,Color.LIGHT_GRAY);

    bold = addStyle("title",regular);
    StyleConstants.setBold(bold,true);

  }

  public void addHistoryItem(String transitionName) {
    fSeq.add(transitionName);
    currentItem = fSeq.size();

    updateText();
  }


  /** Method reinserts the text highlighting the currentItem */
  private void updateText() {
    Enumeration e = fSeq.elements();
    String newS ;
    int count=1;
    Style currentStyle = regular;

    try {
      doc.remove(initText.length(),doc.getLength()-initText.length());


      while (e.hasMoreElements()) {
        newS = (String)e.nextElement();
        if (count==currentItem)
          currentStyle = emph;
        else
          currentStyle = regular;

        doc.insertString(doc.getLength(),newS+"\n",currentStyle);
        count++;
      }
    }catch (BadLocationException b) {
      System.err.println(b.toString());
    }
  }

  public void stepForward() {
    if (currentItem < fSeq.size())
      currentItem++;

    updateText();
  }

  public void stepBackwards() {
    if (currentItem > 1)
      currentItem--;

    updateText();
  }
}