tuned border;
authorwenzelm
Fri, 24 Sep 2010 21:05:07 +0200
changeset 39697 d54242927fb1
parent 39696 f4da0428dc78
child 39698 625a3bc4417b
tuned border;
src/Tools/jEdit/src/jedit/session_dockable.scala
--- a/src/Tools/jEdit/src/jedit/session_dockable.scala	Fri Sep 24 20:33:38 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/session_dockable.scala	Fri Sep 24 21:05:07 2010 +0200
@@ -15,6 +15,7 @@
 import scala.swing.event.{ButtonClicked, SelectionChanged}
 
 import java.awt.BorderLayout
+import javax.swing.border.{BevelBorder, SoftBevelBorder}
 
 import org.gjt.sp.jedit.View
 
@@ -51,8 +52,8 @@
   /* controls */
 
   val session_phase = new Label(Isabelle.session.phase.toString)
-  session_phase.border = Swing.EtchedBorder(Swing.Lowered)
-  session_phase.tooltip = "Prover process status"
+  session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED)
+  session_phase.tooltip = "Prover status"
 
   private val interrupt = new Button("Interrupt") {
     reactions += { case ButtonClicked(_) => Isabelle.session.interrupt }