--- 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)