# HG changeset patch # User wenzelm # Date 1392917012 -3600 # Node ID 0e2b7f04c9440caca399607b38a6923a9ffd5964 # Parent d8eb606cf321531a854e1cc3cf9fd1b88d6f3840 tuned comments; diff -r d8eb606cf321 -r 0e2b7f04c944 src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Thu Feb 20 17:57:26 2014 +0100 +++ b/src/Tools/jEdit/src/rendering.scala Thu Feb 20 18:23:32 2014 +0100 @@ -227,7 +227,7 @@ else None - /* command overview */ + /* command status overview */ val overview_limit = options.int("jedit_text_overview_limit") @@ -265,7 +265,7 @@ } - /* markup selectors */ + /* highlighted area */ private val highlight_elements = Set(Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE, @@ -282,6 +282,8 @@ } + /* hyperlinks */ + private val hyperlink_elements = Set(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL) @@ -342,6 +344,8 @@ } + /* active elements */ + private val active_elements = Set(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW, Markup.SENDBACK, Markup.SIMP_TRACE) @@ -369,6 +373,9 @@ (Command.Results.empty /: results)(_ ++ _) } + + /* tooltip messages */ + private val tooltip_message_elements = Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD) @@ -401,6 +408,8 @@ } + /* tooltips */ + private val tooltips: Map[String, String] = Map( Markup.TOKEN_RANGE -> "inner syntax token", @@ -482,6 +491,8 @@ lazy val tooltip_detach_icon = JEdit_Lib.load_icon(options.string("tooltip_detach_icon")) + /* gutter icons */ + private lazy val gutter_icons = Map( Rendering.information_pri -> JEdit_Lib.load_icon(options.string("gutter_information_icon")), Rendering.warning_pri -> JEdit_Lib.load_icon(options.string("gutter_warning_icon")), @@ -515,6 +526,8 @@ } + /* squiggly underline */ + private val squiggly_colors = Map( Rendering.writeln_pri -> writeln_color, Rendering.information_pri -> information_color, @@ -541,6 +554,8 @@ } + /* message output */ + private val message_colors = Map( Rendering.writeln_pri -> writeln_message_color, Rendering.information_pri -> information_message_color, @@ -575,11 +590,12 @@ message_colors.get(pri).map((_, is_separator)) } - def output_messages(st: Command.State): List[XML.Tree] = st.results.entries.map(_._2).filterNot(Protocol.is_result(_)).toList + /* text background */ + private val background1_elements = Protocol.command_status_markup + Markup.WRITELN_MESSAGE + Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY ++ @@ -623,14 +639,11 @@ } yield Text.Info(r, color) } - def background2(range: Text.Range): List[Text.Info[Color]] = snapshot.select_markup(range, Set(Markup.TOKEN_RANGE), _ => _ => Some(light_color)) - def bullet(range: Text.Range): List[Text.Info[Color]] = - snapshot.select_markup(range, Set(Markup.BULLET), _ => _ => Some(bullet_color)) - + /* text foreground */ private val foreground_elements = Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.CARTOUCHE, Markup.ANTIQUOTED) @@ -643,6 +656,8 @@ }) + /* text color */ + private val text_colors: Map[String, Color] = Map( Markup.KEYWORD1 -> keyword1_color, Markup.KEYWORD2 -> keyword2_color, @@ -685,7 +700,13 @@ } - /* nested text structure -- folds */ + /* virtual bullets */ + + def bullet(range: Text.Range): List[Text.Info[Color]] = + snapshot.select_markup(range, Set(Markup.BULLET), _ => _ => Some(bullet_color)) + + + /* text folds */ private val fold_depth_elements = Set(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)