# HG changeset patch
# User wenzelm
# Date 1285355107 -7200
# Node ID d54242927fb168556e82300ad31605edd9958bd0
# Parent  f4da0428dc786076075bf7fe4990569ad64f011f
tuned border;

diff -r f4da0428dc78 -r d54242927fb1 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 }