merged

--- a/etc/options	Tue Sep 11 22:31:43 2012 +0200
+++ b/etc/options	Tue Sep 11 23:27:19 2012 +0200
@@ -1,6 +1,6 @@
 (* :mode=isabelle-options: *)
 
-section {* Document preparation *}
+section "Document Preparation"
 
 option browser_info : bool = false
   -- "generate theory browser information"
@@ -47,7 +47,7 @@
   -- "additional print modes for prover output (separated by commas)"
 
 
-section {* Parallel checking *}
+section "Parallel Checking"
 
 option threads : int = 0
   -- "maximum number of worker threads for prover process (0 = hardware max.)"
@@ -59,7 +59,7 @@
   -- "threshold for sub-proof parallelization"
 
 
-section {* Detail of proof recording *}
+section "Detail of Proof Recording"
 
 option proofs : int = 1
   -- "level of detail for proof objects: 0, 1, 2"
@@ -69,7 +69,7 @@
   -- "skip over proofs"
 
 
-section {* Global session parameters *}
+section "Global Session Parameters"
 
 option condition : string = ""
   -- "required environment variables for subsequent theories (separated by commas)"
@@ -81,7 +81,7 @@
   -- "timeout for session build job (seconds > 0)"
 
 
-section {* Editor reactivity *}
+section "Editor Reactivity"
 
 option editor_load_delay : real = 0.5
   -- "delay for file load operations (new buffers etc.)"

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/color_value.scala	Tue Sep 11 23:27:19 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/System/options.scala	Tue Sep 11 22:31:43 2012 +0200
+++ b/src/Pure/System/options.scala	Tue Sep 11 23:27:19 2012 +0200
@@ -85,7 +85,7 @@
     val option_entry: Parser[Options => Options] =
     {
       command(SECTION) ~! text ^^
-        { case _ ~ a => (options: Options) => options.set_section(a.trim) } |
+        { case _ ~ a => (options: Options) => options.set_section(a) } |
       command(OPTION) ~! (option_name ~ keyword(":") ~ option_type ~
       keyword("=") ~ option_value ~ (keyword("--") ~! text ^^ { case _ ~ x => x } | success(""))) ^^
         { case _ ~ (a ~ _ ~ b ~ _ ~ c ~ d) => (options: Options) => options.declare(a, b, c, d) }
@@ -150,7 +150,7 @@
 
 
 final class Options private(
-  protected val options: Map[String, Options.Opt] = Map.empty,
+  val options: Map[String, Options.Opt] = Map.empty,
   val section: String = "")
 {
   override def toString: String = options.iterator.mkString("Options (", ",", ")")

--- a/src/Pure/build-jars	Tue Sep 11 22:31:43 2012 +0200
+++ b/src/Pure/build-jars	Tue Sep 11 23:27:19 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 22:31:43 2012 +0200
+++ b/src/Tools/jEdit/etc/options	Tue Sep 11 23:27:19 2012 +0200
@@ -17,3 +17,36 @@
 
 option jedit_tooltip_dismiss_delay : real = 8.0
   -- "global delay for Swing tooltips"
+
+
+section "Rendering of Document Content"
+
+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_options.scala	Tue Sep 11 22:31:43 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_options.scala	Tue Sep 11 23:27:19 2012 +0200
@@ -22,8 +22,15 @@
 
   relevant_options.foreach(Isabelle.options.value.check_name _)
 
-  private val components =
-    Isabelle.options.make_components(List(Isabelle_Logic.logic_selector(false)), relevant_options)
+  private val predefined =
+    Isabelle_Logic.logic_selector(false) ::
+      (for {
+        (name, opt) <- Isabelle.options.value.options.toList
+        // FIXME avoid hard-wired stuff
+        if (name.startsWith("color_") && opt.section == "Rendering of Document Content")
+      } yield Isabelle.options.make_color_component(opt))
+
+  private val components = Isabelle.options.make_components(predefined, relevant_options)
 
   override def _init()
   {

--- a/src/Tools/jEdit/src/isabelle_rendering.scala	Tue Sep 11 22:31:43 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Tue Sep 11 23:27:19 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/jedit_options.scala	Tue Sep 11 22:31:43 2012 +0200
+++ b/src/Tools/jEdit/src/jedit_options.scala	Tue Sep 11 23:27:19 2012 +0200
@@ -14,6 +14,8 @@
 
 import scala.swing.{Component, CheckBox, TextArea}
 
+import org.gjt.sp.jedit.gui.ColorWellButton
+
 
 trait Option_Component extends Component
 {
@@ -24,6 +26,25 @@
 
 class JEdit_Options extends Options_Variable
 {
+  def make_color_component(opt: Options.Opt): Option_Component =
+  {
+    Swing_Thread.require()
+
+    val opt_name = opt.name
+    val opt_title = opt.title("jedit")
+
+    val button = new ColorWellButton(Color_Value(opt.value))
+    val component = new Component with Option_Component {
+      override lazy val peer = button
+      name = opt_name
+      val title = opt_title
+      def load = button.setSelectedColor(Color_Value(string(opt_name)))
+      def save = string(opt_name) = Color_Value.print(button.getSelectedColor)
+    }
+    component.tooltip = Isabelle.tooltip(opt.print_default)
+    component
+  }
+
   def make_component(opt: Options.Opt): Option_Component =
   {
     Swing_Thread.require()

--- a/src/Tools/jEdit/src/session_dockable.scala	Tue Sep 11 22:31:43 2012 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala	Tue Sep 11 23:27:19 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 22:31:43 2012 +0200
+++ b/src/Tools/jEdit/src/text_area_painter.scala	Tue Sep 11 23:27:19 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)
             }
           }