src/Tools/jEdit/src/isabelle_rendering.scala
changeset 49406 38db4832b210
parent 49358 0fa351b1bd14
child 49418 c451856129cd
--- 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 */