provide color values via options;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/color_value.scala	Tue Sep 11 22:54:12 2012 +0200
@@ -0,0 +1,48 @@
+/*  Title:      Pure/General/color_value.scala
+    Module:     PIDE
+    Author:     Makarius
+
+Cached color values.
+*/
+
+package isabelle
+
+
+import java.awt.Color
+
+
+object Color_Value
+{
+  private var cache = Map.empty[String, Color]
+
+  def parse(s: String): Color =
+  {
+    val i = java.lang.Long.parseLong(s, 16)
+    val r = ((i >> 24) & 0xFF).toInt
+    val g = ((i >> 16) & 0xFF).toInt
+    val b = ((i >> 8) & 0xFF).toInt
+    val a = (i & 0xFF).toInt
+    new Color(r, g, b, a)
+  }
+
+  def print(c: Color): String =
+  {
+    val r = new java.lang.Integer(c.getRed)
+    val g = new java.lang.Integer(c.getGreen)
+    val b = new java.lang.Integer(c.getBlue)
+    val a = new java.lang.Integer(c.getAlpha)
+    String.format("%02x%02x%02x%02x", r, g, b, a).toUpperCase
+  }
+
+  def apply(s: String): Color =
+    synchronized {
+      cache.get(s) match {
+        case Some(c) => c
+        case None =>
+          val c = parse(s)
+          cache += (s -> c)
+          c
+      }
+    }
+}
+

--- a/src/Pure/build-jars	Tue Sep 11 20:22:03 2012 +0200
+++ b/src/Pure/build-jars	Tue Sep 11 22:54:12 2012 +0200
@@ -41,6 +41,7 @@
   PIDE/xml.scala
   PIDE/yxml.scala
   System/build.scala
+  System/color_value.scala
   System/command_line.scala
   System/event_bus.scala
   System/gui_setup.scala

--- a/src/Tools/jEdit/etc/options	Tue Sep 11 20:22:03 2012 +0200
+++ b/src/Tools/jEdit/etc/options	Tue Sep 11 22:54:12 2012 +0200
@@ -17,3 +17,36 @@
 
 option jedit_tooltip_dismiss_delay : real = 8.0
   -- "global delay for Swing tooltips"
+
+
+section {* Editor document view *}
+
+option color_outdated : string = "EEE3E3FF"
+option color_unprocessed : string = "FFA0A0FF"
+option color_unprocessed1 : string = "FFA0A032"
+option color_running : string = "610061FF"
+option color_running1 : string = "61006164"
+option color_light : string = "F0F0F0FF"
+option color_writeln : string = "C0C0C0FF"
+option color_warning : string = "FF8C00FF"
+option color_error : string = "B22222FF"
+option color_error1 : string = "B2222232"
+option color_bad : string = "FF6A6A64"
+option color_hilite : string = "FFCC6664"
+option color_quoted : string = "8B8B8B19"
+option color_subexp : string = "50505032"
+option color_hyperlink : string = "000000FF"
+option color_keyword1 : string = "006699FF"
+option color_keyword2 : string = "009966FF"
+
+option color_variable_free : string = "0000FFFF"
+option color_variable_type : string = "A020F0FF"
+option color_variable_skolem : string = "D2691EFF"
+option color_variable_bound : string = "008000FF"
+option color_variable_schematic : string = "00009BFF"
+option color_inner_quoted : string = "D2691EFF"
+option color_inner_comment : string = "8B0000FF"
+option color_inner_numeral : string = "FF0000FF"
+option color_antiquotation : string = "0000FFFF"
+option color_dynamic : string = "7BA428FF"
+

--- a/src/Tools/jEdit/src/isabelle_rendering.scala	Tue Sep 11 20:22:03 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Tue Sep 11 22:54:12 2012 +0200
@@ -13,7 +13,6 @@
 import javax.swing.Icon
 import java.io.{File => JFile}
 
-import org.lobobrowser.util.gui.ColorFactory
 import org.gjt.sp.jedit.syntax.{Token => JEditToken}
 
 import scala.collection.immutable.SortedMap
@@ -23,30 +22,7 @@
 {
   /* physical rendering */
 
-  // see http://www.w3schools.com/cssref/css_colornames.asp
-
-  def get_color(s: String): Color = ColorFactory.getInstance.getColor(s)
-
-  val outdated_color = new Color(238, 227, 227)
-  val unprocessed_color = new Color(255, 160, 160)
-  val unprocessed1_color = new Color(255, 160, 160, 50)
-  val running_color = new Color(97, 0, 97)
-  val running1_color = new Color(97, 0, 97, 100)
-
-  val light_color = new Color(240, 240, 240)
-  val writeln_color = new Color(192, 192, 192)
-  val warning_color = new Color(255, 140, 0)
-  val error_color = new Color(178, 34, 34)
-  val error1_color = new Color(178, 34, 34, 50)
-  val bad_color = new Color(255, 106, 106, 100)
-  val hilite_color = new Color(255, 204, 102, 100)
-
-  val quoted_color = new Color(139, 139, 139, 25)
-  val subexp_color = new Color(80, 80, 80, 50)
-  val hyperlink_color = Color.BLACK
-
-  val keyword1_color = get_color("#006699")
-  val keyword2_color = get_color("#009966")
+  def color_value(s: String): Color = Color_Value(Isabelle.options.value.string(s))
 
   private val writeln_pri = 1
   private val warning_pri = 2
@@ -76,11 +52,11 @@
           ((Protocol.Status.init, 0) /: results) {
             case ((s1, p1), Text.Info(_, (s2, p2))) => (s1 + s2, p1 max p2) }
 
-        if (pri == warning_pri) Some(warning_color)
-        else if (pri == error_pri) Some(error_color)
-        else if (status.is_unprocessed) Some(unprocessed_color)
-        else if (status.is_running) Some(running_color)
-        else if (status.is_failed) Some(error_color)
+        if (pri == warning_pri) Some(color_value("color_warning"))
+        else if (pri == error_pri) Some(color_value("color_error"))
+        else if (status.is_unprocessed) Some(color_value("color_unprocessed"))
+        else if (status.is_running) Some(color_value("color_running"))
+        else if (status.is_failed) Some(color_value("color_error"))
         else None
       }
     }
@@ -101,7 +77,7 @@
     snapshot.select_markup(range, Some(subexp_include),
         {
           case Text.Info(info_range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
-            Text.Info(snapshot.convert(info_range), subexp_color)
+            Text.Info(snapshot.convert(info_range), color_value("color_subexp"))
         }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
   }
 
@@ -250,13 +226,13 @@
   }
 
 
-  private val squiggly_colors = Map(
-    writeln_pri -> writeln_color,
-    warning_pri -> warning_color,
-    error_pri -> error_color)
-
   def squiggly_underline(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
   {
+    val squiggly_colors = Map(
+      writeln_pri -> color_value("color_writeln"),
+      warning_pri -> color_value("color_warning"),
+      error_pri -> color_value("color_error"))
+
     val results =
       snapshot.cumulate_markup[Int](range, 0,
         Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
@@ -278,7 +254,7 @@
 
   def background1(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
   {
-    if (snapshot.is_outdated) Stream(Text.Info(range, outdated_color))
+    if (snapshot.is_outdated) Stream(Text.Info(range, color_value("color_outdated")))
     else
       for {
         Text.Info(r, result) <-
@@ -290,15 +266,15 @@
               if (Protocol.command_status_markup(markup.name)) =>
                 (Some(Protocol.command_status(status, markup)), color)
               case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.BAD, _), _))) =>
-                (None, Some(bad_color))
+                (None, Some(color_value("color_bad")))
               case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.HILITE, _), _))) =>
-                (None, Some(hilite_color))
+                (None, Some(color_value("color_hilite")))
             })
         color <-
           (result match {
             case (Some(status), opt_color) =>
-              if (status.is_unprocessed) Some(unprocessed1_color)
-              else if (status.is_running) Some(running1_color)
+              if (status.is_unprocessed) Some(color_value("color_unprocessed1"))
+              else if (status.is_running) Some(color_value("color_running1"))
               else opt_color
             case (_, opt_color) => opt_color
           })
@@ -310,7 +286,8 @@
     snapshot.select_markup(range,
       Some(Set(Isabelle_Markup.TOKEN_RANGE)),
       {
-        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.TOKEN_RANGE, _), _)) => light_color
+        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.TOKEN_RANGE, _), _)) =>
+          color_value("color_light")
       })
 
 
@@ -318,45 +295,49 @@
     snapshot.select_markup(range,
       Some(Set(Isabelle_Markup.STRING, Isabelle_Markup.ALTSTRING, Isabelle_Markup.VERBATIM)),
       {
-        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.STRING, _), _)) => quoted_color
-        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ALTSTRING, _), _)) => quoted_color
-        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.VERBATIM, _), _)) => quoted_color
+        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.STRING, _), _)) =>
+          color_value("color_quoted")
+        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ALTSTRING, _), _)) =>
+          color_value("color_quoted")
+        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.VERBATIM, _), _)) =>
+          color_value("color_quoted")
       })
 
 
-  private val text_colors: Map[String, Color] =
-    Map(
-      Isabelle_Markup.STRING -> get_color("black"),
-      Isabelle_Markup.ALTSTRING -> get_color("black"),
-      Isabelle_Markup.VERBATIM -> get_color("black"),
-      Isabelle_Markup.LITERAL -> keyword1_color,
-      Isabelle_Markup.DELIMITER -> get_color("black"),
-      Isabelle_Markup.TFREE -> get_color("#A020F0"),
-      Isabelle_Markup.TVAR -> get_color("#A020F0"),
-      Isabelle_Markup.FREE -> get_color("blue"),
-      Isabelle_Markup.SKOLEM -> get_color("#D2691E"),
-      Isabelle_Markup.BOUND -> get_color("green"),
-      Isabelle_Markup.VAR -> get_color("#00009B"),
-      Isabelle_Markup.INNER_STRING -> get_color("#D2691E"),
-      Isabelle_Markup.INNER_COMMENT -> get_color("#8B0000"),
-      Isabelle_Markup.DYNAMIC_FACT -> get_color("#7BA428"),
-      Isabelle_Markup.ML_KEYWORD -> keyword1_color,
-      Isabelle_Markup.ML_DELIMITER -> get_color("black"),
-      Isabelle_Markup.ML_NUMERAL -> get_color("red"),
-      Isabelle_Markup.ML_CHAR -> get_color("#D2691E"),
-      Isabelle_Markup.ML_STRING -> get_color("#D2691E"),
-      Isabelle_Markup.ML_COMMENT -> get_color("#8B0000"),
-      Isabelle_Markup.ANTIQ -> get_color("blue"))
-
-  private val text_color_elements = Set.empty[String] ++ text_colors.keys
-
   def text_color(snapshot: Document.Snapshot, range: Text.Range, color: Color)
       : Stream[Text.Info[Color]] =
+  {
+    val text_colors: Map[String, Color] = Map(
+      Isabelle_Markup.STRING -> Color.BLACK,
+      Isabelle_Markup.ALTSTRING -> Color.BLACK,
+      Isabelle_Markup.VERBATIM -> Color.BLACK,
+      Isabelle_Markup.LITERAL -> color_value("color_keyword1"),
+      Isabelle_Markup.DELIMITER -> Color.BLACK,
+      Isabelle_Markup.TFREE -> color_value("color_variable_type"),
+      Isabelle_Markup.TVAR -> color_value("color_variable_type"),
+      Isabelle_Markup.FREE -> color_value("color_variable_free"),
+      Isabelle_Markup.SKOLEM -> color_value("color_variable_skolem"),
+      Isabelle_Markup.BOUND -> color_value("color_variable_bound"),
+      Isabelle_Markup.VAR -> color_value("color_variable_schematic"),
+      Isabelle_Markup.INNER_STRING -> color_value("color_inner_quoted"),
+      Isabelle_Markup.INNER_COMMENT -> color_value("color_inner_comment"),
+      Isabelle_Markup.DYNAMIC_FACT -> color_value("color_dynamic"),
+      Isabelle_Markup.ML_KEYWORD -> color_value("color_keyword1"),
+      Isabelle_Markup.ML_DELIMITER -> Color.BLACK,
+      Isabelle_Markup.ML_NUMERAL -> color_value("color_inner_numeral"),
+      Isabelle_Markup.ML_CHAR -> color_value("color_inner_quoted"),
+      Isabelle_Markup.ML_STRING -> color_value("color_inner_quoted"),
+      Isabelle_Markup.ML_COMMENT -> color_value("color_inner_comment"),
+      Isabelle_Markup.ANTIQ -> color_value("color_antiquotation"))
+
+    val text_color_elements = Set.empty[String] ++ text_colors.keys
+
     snapshot.cumulate_markup(range, color, Some(text_color_elements),
       {
         case (_, Text.Info(_, XML.Elem(Markup(m, _), _)))
         if text_colors.isDefinedAt(m) => text_colors(m)
       })
+  }
 
 
   /* token markup -- text styles */

--- a/src/Tools/jEdit/src/session_dockable.scala	Tue Sep 11 20:22:03 2012 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala	Tue Sep 11 22:54:12 2012 +0200
@@ -89,10 +89,10 @@
           var end = size.width - insets.right
           for {
             (n, color) <- List(
-              (st.unprocessed, Isabelle_Rendering.unprocessed1_color),
-              (st.running, Isabelle_Rendering.running_color),
-              (st.warned, Isabelle_Rendering.warning_color),
-              (st.failed, Isabelle_Rendering.error_color)) }
+              (st.unprocessed, Isabelle_Rendering.color_value("color_unprocessed1")),
+              (st.running, Isabelle_Rendering.color_value("color_running")),
+              (st.warned, Isabelle_Rendering.color_value("color_warning")),
+              (st.failed, Isabelle_Rendering.color_value("color_error"))) }
           {
             gfx.setColor(color)
             val v = (n * w / st.total) max (if (n > 0) 2 else 0)

--- a/src/Tools/jEdit/src/text_area_painter.scala	Tue Sep 11 20:22:03 2012 +0200
+++ b/src/Tools/jEdit/src/text_area_painter.scala	Tue Sep 11 22:54:12 2012 +0200
@@ -312,7 +312,7 @@
               Text.Info(range, _) <- info.try_restrict(line_range)
               r <- gfx_range(range)
             } {
-              gfx.setColor(Isabelle_Rendering.hyperlink_color)
+              gfx.setColor(Isabelle_Rendering.color_value("color_hyperlink"))
               gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
             }
           }