src/Tools/jEdit/src/rendering.scala
changeset 52873 9e934d4fff00
parent 52650 4cf6fbf1d9a1
child 52889 ea3338812e67
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Mon Aug 05 21:23:06 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Mon Aug 05 22:54:50 2013 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4  import javax.swing.Icon
     1.5  
     1.6  import org.gjt.sp.jedit.syntax.{Token => JEditToken}
     1.7 -import org.gjt.sp.jedit.{jEdit, GUIUtilities}
     1.8 +import org.gjt.sp.jedit.jEdit
     1.9  
    1.10  import scala.collection.immutable.SortedMap
    1.11  
    1.12 @@ -41,23 +41,6 @@
    1.13      Markup.ERROR -> error_pri, Markup.ERROR_MESSAGE -> error_pri)
    1.14  
    1.15  
    1.16 -  /* icons */
    1.17 -
    1.18 -  def load_icon(name: String): Icon =
    1.19 -  {
    1.20 -    val name1 =
    1.21 -      if (name.startsWith("idea-icons/")) {
    1.22 -        val file =
    1.23 -          Isabelle_System.platform_file_url(Path.explode("$JEDIT_HOME/dist/jars/idea-icons.jar"))
    1.24 -        "jar:" + file + "!/" + name
    1.25 -      }
    1.26 -      else name
    1.27 -    val icon = GUIUtilities.loadIcon(name1)
    1.28 -    if (icon.getIconWidth < 0 || icon.getIconHeight < 0) error("Bad icon: " + name)
    1.29 -    else icon
    1.30 -  }
    1.31 -
    1.32 -
    1.33    /* jEdit font */
    1.34  
    1.35    def font_family(): String = jEdit.getProperty("view.font")
    1.36 @@ -381,15 +364,15 @@
    1.37    val tooltip_margin: Int = options.int("jedit_tooltip_margin")
    1.38    val tooltip_bounds: Double = (options.real("jedit_tooltip_bounds") max 0.2) min 0.8
    1.39  
    1.40 -  lazy val tooltip_close_icon = Rendering.load_icon(options.string("tooltip_close_icon"))
    1.41 -  lazy val tooltip_detach_icon = Rendering.load_icon(options.string("tooltip_detach_icon"))
    1.42 +  lazy val tooltip_close_icon = JEdit_Lib.load_icon(options.string("tooltip_close_icon"))
    1.43 +  lazy val tooltip_detach_icon = JEdit_Lib.load_icon(options.string("tooltip_detach_icon"))
    1.44  
    1.45  
    1.46    private lazy val gutter_icons = Map(
    1.47 -    Rendering.information_pri -> Rendering.load_icon(options.string("gutter_information_icon")),
    1.48 -    Rendering.warning_pri -> Rendering.load_icon(options.string("gutter_warning_icon")),
    1.49 -    Rendering.legacy_pri -> Rendering.load_icon(options.string("gutter_legacy_icon")),
    1.50 -    Rendering.error_pri -> Rendering.load_icon(options.string("gutter_error_icon")))
    1.51 +    Rendering.information_pri -> JEdit_Lib.load_icon(options.string("gutter_information_icon")),
    1.52 +    Rendering.warning_pri -> JEdit_Lib.load_icon(options.string("gutter_warning_icon")),
    1.53 +    Rendering.legacy_pri -> JEdit_Lib.load_icon(options.string("gutter_legacy_icon")),
    1.54 +    Rendering.error_pri -> JEdit_Lib.load_icon(options.string("gutter_error_icon")))
    1.55  
    1.56    private val gutter_elements = Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
    1.57