tuned options (again);

--- a/src/Tools/jEdit/etc/options	Fri Sep 14 12:29:02 2012 +0200
+++ b/src/Tools/jEdit/etc/options	Fri Sep 14 12:46:33 2012 +0200
@@ -21,32 +21,33 @@
 
 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 outdated_color : string = "EEE3E3FF"
+option unprocessed_color : string = "FFA0A0FF"
+option unprocessed1_color : string = "FFA0A032"
+option running_color : string = "610061FF"
+option running1_color : string = "61006164"
+option light_color : string = "F0F0F0FF"
+option writeln_color : string = "C0C0C0FF"
+option warning_color : string = "FF8C00FF"
+option error_color : string = "B22222FF"
+option error1_color : string = "B2222232"
+option bad_color : string = "FF6A6A64"
+option hilite_color : string = "FFCC6664"
+option quoted_color : string = "8B8B8B19"
+option subexp_color : string = "50505032"
+option hyperlink_color : string = "000000FF"
+option keyword1_color : string = "006699FF"
+option keyword2_color : 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"
+option tfree_color : string = "A020F0FF"
+option tvar_color : string = "A020F0FF"
+option free_color : string = "0000FFFF"
+option skolem_color : string = "D2691EFF"
+option bound_color : string = "008000FF"
+option var_color : string = "00009BFF"
+option inner_numeral_color : string = "FF0000FF"
+option inner_quoted_color : string = "D2691EFF"
+option inner_comment_color : string = "8B0000FF"
+option antiquotation_color : string = "0000FFFF"
+option dynamic_color : string = "7BA428FF"
 

--- a/src/Tools/jEdit/src/isabelle_options.scala	Fri Sep 14 12:29:02 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_options.scala	Fri Sep 14 12:46:33 2012 +0200
@@ -58,7 +58,7 @@
   private val predefined =
     (for {
       (name, opt) <- Isabelle.options.value.options.toList
-      if (name.startsWith("color_") && opt.section == "Rendering of Document Content")
+      if (name.endsWith("_color") && opt.section == "Rendering of Document Content")
     } yield Isabelle.options.make_color_component(opt))
 
   assert(!predefined.isEmpty)

--- a/src/Tools/jEdit/src/isabelle_rendering.scala	Fri Sep 14 12:29:02 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Fri Sep 14 12:46:33 2012 +0200
@@ -52,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(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"))
+        if (pri == warning_pri) Some(color_value("warning_color"))
+        else if (pri == error_pri) Some(color_value("error_color"))
+        else if (status.is_unprocessed) Some(color_value("unprocessed_color"))
+        else if (status.is_running) Some(color_value("running_color"))
+        else if (status.is_failed) Some(color_value("error_color"))
         else None
       }
     }
@@ -77,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), color_value("color_subexp"))
+            Text.Info(snapshot.convert(info_range), color_value("subexp_color"))
         }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
   }
 
@@ -230,9 +230,9 @@
   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"))
+      writeln_pri -> color_value("writeln_color"),
+      warning_pri -> color_value("warning_color"),
+      error_pri -> color_value("error_color"))
 
     val results =
       snapshot.cumulate_markup[Int](range, 0,
@@ -255,7 +255,7 @@
 
   def background1(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
   {
-    if (snapshot.is_outdated) Stream(Text.Info(range, color_value("color_outdated")))
+    if (snapshot.is_outdated) Stream(Text.Info(range, color_value("outdated_color")))
     else
       for {
         Text.Info(r, result) <-
@@ -267,15 +267,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(color_value("color_bad")))
+                (None, Some(color_value("bad_color")))
               case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.HILITE, _), _))) =>
-                (None, Some(color_value("color_hilite")))
+                (None, Some(color_value("hilite_color")))
             })
         color <-
           (result match {
             case (Some(status), opt_color) =>
-              if (status.is_unprocessed) Some(color_value("color_unprocessed1"))
-              else if (status.is_running) Some(color_value("color_running1"))
+              if (status.is_unprocessed) Some(color_value("unprocessed1_color"))
+              else if (status.is_running) Some(color_value("running1_color"))
               else opt_color
             case (_, opt_color) => opt_color
           })
@@ -288,7 +288,7 @@
       Some(Set(Isabelle_Markup.TOKEN_RANGE)),
       {
         case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.TOKEN_RANGE, _), _)) =>
-          color_value("color_light")
+          color_value("light_color")
       })
 
 
@@ -297,11 +297,11 @@
       Some(Set(Isabelle_Markup.STRING, Isabelle_Markup.ALTSTRING, Isabelle_Markup.VERBATIM)),
       {
         case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.STRING, _), _)) =>
-          color_value("color_quoted")
+          color_value("quoted_color")
         case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ALTSTRING, _), _)) =>
-          color_value("color_quoted")
+          color_value("quoted_color")
         case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.VERBATIM, _), _)) =>
-          color_value("color_quoted")
+          color_value("quoted_color")
       })
 
 
@@ -312,24 +312,24 @@
       Isabelle_Markup.STRING -> Color.BLACK,
       Isabelle_Markup.ALTSTRING -> Color.BLACK,
       Isabelle_Markup.VERBATIM -> Color.BLACK,
-      Isabelle_Markup.LITERAL -> color_value("color_keyword1"),
+      Isabelle_Markup.LITERAL -> color_value("keyword1_color"),
       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.TFREE -> color_value("tfree_color"),
+      Isabelle_Markup.TVAR -> color_value("tvar_color"),
+      Isabelle_Markup.FREE -> color_value("free_color"),
+      Isabelle_Markup.SKOLEM -> color_value("skolem_color"),
+      Isabelle_Markup.BOUND -> color_value("bound_color"),
+      Isabelle_Markup.VAR -> color_value("var_color"),
+      Isabelle_Markup.INNER_STRING -> color_value("inner_quoted_color"),
+      Isabelle_Markup.INNER_COMMENT -> color_value("inner_comment_color"),
+      Isabelle_Markup.DYNAMIC_FACT -> color_value("dynamic_color"),
+      Isabelle_Markup.ML_KEYWORD -> color_value("keyword1_color"),
       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"))
+      Isabelle_Markup.ML_NUMERAL -> color_value("inner_numeral_color"),
+      Isabelle_Markup.ML_CHAR -> color_value("inner_quoted_color"),
+      Isabelle_Markup.ML_STRING -> color_value("inner_quoted_color"),
+      Isabelle_Markup.ML_COMMENT -> color_value("inner_comment_color"),
+      Isabelle_Markup.ANTIQ -> color_value("antiquotation_color"))
 
     val text_color_elements = Set.empty[String] ++ text_colors.keys
 

--- a/src/Tools/jEdit/src/session_dockable.scala	Fri Sep 14 12:29:02 2012 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala	Fri Sep 14 12:46:33 2012 +0200
@@ -89,10 +89,10 @@
           var end = size.width - insets.right
           for {
             (n, color) <- List(
-              (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"))) }
+              (st.unprocessed, Isabelle_Rendering.color_value("unprocessed1_color")),
+              (st.running, Isabelle_Rendering.color_value("running_color")),
+              (st.warned, Isabelle_Rendering.color_value("warning_color")),
+              (st.failed, Isabelle_Rendering.color_value("error_color"))) }
           {
             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	Fri Sep 14 12:29:02 2012 +0200
+++ b/src/Tools/jEdit/src/text_area_painter.scala	Fri Sep 14 12:46:33 2012 +0200
@@ -312,7 +312,7 @@
               Text.Info(range, _) <- info.try_restrict(line_range)
               r <- gfx_range(range)
             } {
-              gfx.setColor(Isabelle_Rendering.color_value("color_hyperlink"))
+              gfx.setColor(Isabelle_Rendering.color_value("hyperlink_color"))
               gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
             }
           }

--- a/src/Tools/jEdit/src/text_overview.scala	Fri Sep 14 12:29:02 2012 +0200
+++ b/src/Tools/jEdit/src/text_overview.scala	Fri Sep 14 12:46:33 2012 +0200
@@ -69,7 +69,7 @@
         val snapshot = doc_view.model.snapshot()
 
         if (snapshot.is_outdated) {
-          gfx.setColor(Isabelle_Rendering.color_value("color_outdated"))
+          gfx.setColor(Isabelle_Rendering.color_value("outdated_color"))
           gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
         }
         else {