src/Tools/jEdit/src/token_markup.scala
changeset 57126 3a928dffc37f
parent 56662 f373fb77e0a4
child 57612 990ffb84489b
equal deleted inserted replaced
57116:85e55ea7e06d 57126:3a928dffc37f
   102         else font1
   102         else font1
   103       })
   103       })
   104   }
   104   }
   105 
   105 
   106   private def bold_style(style: SyntaxStyle): SyntaxStyle =
   106   private def bold_style(style: SyntaxStyle): SyntaxStyle =
   107     font_style(style, _.deriveFont(Font.BOLD))
   107     font_style(style, font => font.deriveFont(if (font.isBold) Font.PLAIN else Font.BOLD))
   108 
   108 
   109   val hidden_color: Color = new Color(255, 255, 255, 0)
   109   val hidden_color: Color = new Color(255, 255, 255, 0)
   110 
   110 
   111   class Style_Extender extends SyntaxUtilities.StyleExtender
   111   class Style_Extender extends SyntaxUtilities.StyleExtender
   112   {
   112   {