src/Tools/jEdit/src/jedit_lib.scala
changeset 52873 9e934d4fff00
parent 52478 0a1db0d02628
child 52874 91032244e4ca
     1.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Mon Aug 05 21:23:06 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Mon Aug 05 22:54:50 2013 +0200
     1.3 @@ -10,10 +10,11 @@
     1.4  import isabelle._
     1.5  
     1.6  import java.awt.{Component, Container, Window, GraphicsEnvironment, Point, Rectangle}
     1.7 +import javax.swing.Icon
     1.8  
     1.9  import scala.annotation.tailrec
    1.10  
    1.11 -import org.gjt.sp.jedit.{jEdit, Buffer, View}
    1.12 +import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities}
    1.13  import org.gjt.sp.jedit.buffer.JEditBuffer
    1.14  import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter}
    1.15  
    1.16 @@ -222,5 +223,22 @@
    1.17        val average = string_width("mix") / (3 * unit)
    1.18        def apply(s: String): Double = if (s == "\n") 1.0 else string_width(s) / unit
    1.19      }
    1.20 +
    1.21 +
    1.22 +  /* icons */
    1.23 +
    1.24 +  def load_icon(name: String): Icon =
    1.25 +  {
    1.26 +    val name1 =
    1.27 +      if (name.startsWith("idea-icons/")) {
    1.28 +        val file =
    1.29 +          Isabelle_System.platform_file_url(Path.explode("$JEDIT_HOME/dist/jars/idea-icons.jar"))
    1.30 +        "jar:" + file + "!/" + name
    1.31 +      }
    1.32 +      else name
    1.33 +    val icon = GUIUtilities.loadIcon(name1)
    1.34 +    if (icon.getIconWidth < 0 || icon.getIconHeight < 0) error("Bad icon: " + name)
    1.35 +    else icon
    1.36 +  }
    1.37  }
    1.38