# HG changeset patch # User wenzelm # Date 1347396852 -7200 # Node ID a600c017f814980be05eae143042eee8bab3be53 # Parent afcccb9bfa3bd591555df752d8615e4764ce6068 provide color values via options; diff -r afcccb9bfa3b -r a600c017f814 src/Pure/System/color_value.scala --- /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 + } + } +} + diff -r afcccb9bfa3b -r a600c017f814 src/Pure/build-jars --- 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 diff -r afcccb9bfa3b -r a600c017f814 src/Tools/jEdit/etc/options --- 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" + diff -r afcccb9bfa3b -r a600c017f814 src/Tools/jEdit/src/isabelle_rendering.scala --- 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 */ diff -r afcccb9bfa3b -r a600c017f814 src/Tools/jEdit/src/session_dockable.scala --- 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) diff -r afcccb9bfa3b -r a600c017f814 src/Tools/jEdit/src/text_area_painter.scala --- 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) } }