# HG changeset patch # User wenzelm # Date 1375736090 -7200 # Node ID 9e934d4fff0072b0569f136f1b8f5d6b10eb2a06 # Parent 8d8cb75ab20a9f5a717da35c9ebf8f279d60d883 tuned signature; diff -r 8d8cb75ab20a -r 9e934d4fff00 src/Tools/jEdit/src/jedit_lib.scala --- a/src/Tools/jEdit/src/jedit_lib.scala Mon Aug 05 21:23:06 2013 +0200 +++ b/src/Tools/jEdit/src/jedit_lib.scala Mon Aug 05 22:54:50 2013 +0200 @@ -10,10 +10,11 @@ import isabelle._ import java.awt.{Component, Container, Window, GraphicsEnvironment, Point, Rectangle} +import javax.swing.Icon import scala.annotation.tailrec -import org.gjt.sp.jedit.{jEdit, Buffer, View} +import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities} import org.gjt.sp.jedit.buffer.JEditBuffer import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter} @@ -222,5 +223,22 @@ val average = string_width("mix") / (3 * unit) def apply(s: String): Double = if (s == "\n") 1.0 else string_width(s) / unit } + + + /* icons */ + + def load_icon(name: String): Icon = + { + val name1 = + if (name.startsWith("idea-icons/")) { + val file = + Isabelle_System.platform_file_url(Path.explode("$JEDIT_HOME/dist/jars/idea-icons.jar")) + "jar:" + file + "!/" + name + } + else name + val icon = GUIUtilities.loadIcon(name1) + if (icon.getIconWidth < 0 || icon.getIconHeight < 0) error("Bad icon: " + name) + else icon + } } diff -r 8d8cb75ab20a -r 9e934d4fff00 src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Mon Aug 05 21:23:06 2013 +0200 +++ b/src/Tools/jEdit/src/rendering.scala Mon Aug 05 22:54:50 2013 +0200 @@ -14,7 +14,7 @@ import javax.swing.Icon import org.gjt.sp.jedit.syntax.{Token => JEditToken} -import org.gjt.sp.jedit.{jEdit, GUIUtilities} +import org.gjt.sp.jedit.jEdit import scala.collection.immutable.SortedMap @@ -41,23 +41,6 @@ Markup.ERROR -> error_pri, Markup.ERROR_MESSAGE -> error_pri) - /* icons */ - - def load_icon(name: String): Icon = - { - val name1 = - if (name.startsWith("idea-icons/")) { - val file = - Isabelle_System.platform_file_url(Path.explode("$JEDIT_HOME/dist/jars/idea-icons.jar")) - "jar:" + file + "!/" + name - } - else name - val icon = GUIUtilities.loadIcon(name1) - if (icon.getIconWidth < 0 || icon.getIconHeight < 0) error("Bad icon: " + name) - else icon - } - - /* jEdit font */ def font_family(): String = jEdit.getProperty("view.font") @@ -381,15 +364,15 @@ val tooltip_margin: Int = options.int("jedit_tooltip_margin") val tooltip_bounds: Double = (options.real("jedit_tooltip_bounds") max 0.2) min 0.8 - lazy val tooltip_close_icon = Rendering.load_icon(options.string("tooltip_close_icon")) - lazy val tooltip_detach_icon = Rendering.load_icon(options.string("tooltip_detach_icon")) + lazy val tooltip_close_icon = JEdit_Lib.load_icon(options.string("tooltip_close_icon")) + lazy val tooltip_detach_icon = JEdit_Lib.load_icon(options.string("tooltip_detach_icon")) private lazy val gutter_icons = Map( - Rendering.information_pri -> Rendering.load_icon(options.string("gutter_information_icon")), - Rendering.warning_pri -> Rendering.load_icon(options.string("gutter_warning_icon")), - Rendering.legacy_pri -> Rendering.load_icon(options.string("gutter_legacy_icon")), - Rendering.error_pri -> Rendering.load_icon(options.string("gutter_error_icon"))) + Rendering.information_pri -> JEdit_Lib.load_icon(options.string("gutter_information_icon")), + Rendering.warning_pri -> JEdit_Lib.load_icon(options.string("gutter_warning_icon")), + Rendering.legacy_pri -> JEdit_Lib.load_icon(options.string("gutter_legacy_icon")), + Rendering.error_pri -> JEdit_Lib.load_icon(options.string("gutter_error_icon"))) private val gutter_elements = Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)