# HG changeset patch # User wenzelm # Date 1347619593 -7200 # Node ID 7d1af0a6e7974f5d0f8fafcdfa49924aafb64090 # Parent 65c6a1d62dbcc6d4d1c574fa836c17ad8cd5574a tuned options (again); diff -r 65c6a1d62dbc -r 7d1af0a6e797 src/Tools/jEdit/etc/options --- 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" diff -r 65c6a1d62dbc -r 7d1af0a6e797 src/Tools/jEdit/src/isabelle_options.scala --- 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) diff -r 65c6a1d62dbc -r 7d1af0a6e797 src/Tools/jEdit/src/isabelle_rendering.scala --- 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 diff -r 65c6a1d62dbc -r 7d1af0a6e797 src/Tools/jEdit/src/session_dockable.scala --- 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) diff -r 65c6a1d62dbc -r 7d1af0a6e797 src/Tools/jEdit/src/text_area_painter.scala --- 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) } } diff -r 65c6a1d62dbc -r 7d1af0a6e797 src/Tools/jEdit/src/text_overview.scala --- 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 {