--- a/src/Tools/jEdit/src/isabelle_rendering.scala Mon Sep 17 15:52:50 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala Mon Sep 17 17:49:11 2012 +0200
@@ -14,6 +14,8 @@
import java.io.{File => JFile}
import org.gjt.sp.jedit.syntax.{Token => JEditToken}
+import org.gjt.sp.jedit.GUIUtilities
+import org.gjt.sp.util.Log
import scala.collection.immutable.SortedMap
@@ -24,17 +26,28 @@
new Isabelle_Rendering(snapshot, options)
- /* physical rendering */
+ /* message priorities */
private val writeln_pri = 1
private val warning_pri = 2
private val legacy_pri = 3
private val error_pri = 4
+
+ /* icons */
+
+ private def load_icon(name: String): Icon =
+ {
+ val icon = GUIUtilities.loadIcon(name)
+ if (icon.getIconWidth < 0 || icon.getIconHeight < 0)
+ Log.log(Log.ERROR, icon, "Bad icon: " + name)
+ icon
+ }
+
private val gutter_icons = Map(
- warning_pri -> Isabelle.load_icon("16x16/status/dialog-information.png"),
- legacy_pri -> Isabelle.load_icon("16x16/status/dialog-warning.png"),
- error_pri -> Isabelle.load_icon("16x16/status/dialog-error.png"))
+ warning_pri -> load_icon("16x16/status/dialog-information.png"),
+ legacy_pri -> load_icon("16x16/status/dialog-warning.png"),
+ error_pri -> load_icon("16x16/status/dialog-error.png"))
/* token markup -- text styles */