--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/GraphBrowser/awt/Border.java Fri Jul 16 12:55:02 2021 +0200
@@ -0,0 +1,39 @@
+/***************************************************************************
+ Title: awt/Border.java
+ Author: Stefan Berghofer, TU Muenchen
+
+ This class defines a nice 3D border.
+***************************************************************************/
+
+package isabelle.awt;
+
+import java.awt.*;
+
+public class Border extends Panel {
+ int bs;
+
+ public Insets getInsets() {
+ return new Insets(bs*3/2,bs*3/2,bs*3/2,bs*3/2);
+ }
+
+ public Border(Component comp,int s) {
+ setLayout(new GridLayout(1,1));
+ add(comp);
+ bs=s;
+ }
+
+ public void paint(Graphics g) {
+ int w = getSize().width;
+ int h = getSize().height;
+ int x1[]={0,bs,w-bs,w}, y1[]={0,bs,bs,0};
+ int x2[]={w,w-bs,w-bs,w}, y2[]={0,bs,h-bs,h};
+ int y3[]={h,h-bs,h-bs,h};
+
+ g.setColor(new Color(224,224,224));
+ g.fillPolygon(y1,y2,4);
+ g.fillPolygon(x1,y1,4);
+ g.setColor(Color.gray);
+ g.fillPolygon(x2,y2,4);
+ g.fillPolygon(x1,y3,4);
+ }
+}