# HG changeset patch
# User wenzelm
# Date 1353865813 -3600
# Node ID 2c94c065564ecbaf8acb640ec953764c8877e364
# Parent  6d04e2422769cc1c4d5bbbd9554da3f2c4982ecf
prefer strict error;

diff -r 6d04e2422769 -r 2c94c065564e src/Tools/jEdit/src/isabelle_rendering.scala
--- a/src/Tools/jEdit/src/isabelle_rendering.scala	Sun Nov 25 18:47:33 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Sun Nov 25 18:50:13 2012 +0100
@@ -15,7 +15,6 @@
 
 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
 
@@ -46,9 +45,8 @@
   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
+    if (icon.getIconWidth < 0 || icon.getIconHeight < 0) error("Bad icon: " + name)
+    else icon
   }
 
   private val gutter_icons = Map(