src/Tools/GraphBrowser/graphbrowser/Box.java
author wenzelm
Wed, 13 Aug 2025 19:40:09 +0200
changeset 83005 a2a860cd3215
parent 74015 12b1f4649ab1
permissions -rw-r--r--
more robust, notably for Isabelle/MAWEN "polyminus.sml matchsub (?a * (?b - ?c)...";

/***************************************************************************
  Title:      graphbrowser/Box.java
  Author:     Gerwin Klein, TU Muenchen

  A box with width and height. Used instead of java.awt.Dimension for 
  batch mode.

***************************************************************************/

package isabelle.graphbrowser;

public class Box {
  public int width;
  public int height;

  public Box(int w, int h) {
    this.width = w;
    this.height = h;
  }
}