equal
deleted
inserted
replaced
125 |
125 |
126 |
126 |
127 /* icon */ |
127 /* icon */ |
128 |
128 |
129 def isabelle_icon(): ImageIcon = |
129 def isabelle_icon(): ImageIcon = |
130 new ImageIcon(getClass.getClassLoader.getResource("isabelle/isabelle.gif")) |
130 new ImageIcon(getClass.getClassLoader.getResource("isabelle/isabelle-icon.gif")) |
131 |
131 |
132 def isabelle_image(): Image = isabelle_icon().getImage |
132 def isabelle_image(): Image = isabelle_icon().getImage |
133 |
133 |
134 |
134 |
135 /* component hierachy */ |
135 /* component hierachy */ |