1.1 --- a/src/Tools/jEdit/src/rendering.scala Fri Feb 21 12:32:06 2014 +0100
1.2 +++ b/src/Tools/jEdit/src/rendering.scala Fri Feb 21 12:57:14 2014 +0100
1.3 @@ -146,6 +146,75 @@
1.4 else if (ML_Lex.keywords2(token.source)) JEditToken.KEYWORD2
1.5 else if (ML_Lex.keywords3(token.source)) JEditToken.KEYWORD3
1.6 else JEditToken.KEYWORD1
1.7 +
1.8 +
1.9 + /* markup elements */
1.10 +
1.11 + private val completion_elements =
1.12 + Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
1.13 + Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE,
1.14 + Markup.ML_STRING, Markup.ML_COMMENT)
1.15 +
1.16 + private val highlight_elements =
1.17 + Set(Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE,
1.18 + Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING,
1.19 + Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
1.20 + Markup.VAR, Markup.TFREE, Markup.TVAR)
1.21 +
1.22 + private val hyperlink_elements =
1.23 + Set(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL)
1.24 +
1.25 + private val active_elements =
1.26 + Set(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
1.27 + Markup.SENDBACK, Markup.SIMP_TRACE)
1.28 +
1.29 + private val tooltip_message_elements =
1.30 + Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)
1.31 +
1.32 + private val tooltip_descriptions =
1.33 + Map(
1.34 + Markup.TOKEN_RANGE -> "inner syntax token",
1.35 + Markup.FREE -> "free variable",
1.36 + Markup.SKOLEM -> "skolem variable",
1.37 + Markup.BOUND -> "bound variable",
1.38 + Markup.VAR -> "schematic variable",
1.39 + Markup.TFREE -> "free type variable",
1.40 + Markup.TVAR -> "schematic type variable")
1.41 +
1.42 + private val tooltip_elements =
1.43 + Set(Markup.LANGUAGE, Markup.TIMING, Markup.ENTITY, Markup.SORTING,
1.44 + Markup.TYPING, Markup.ML_TYPING, Markup.PATH, Markup.URL) ++
1.45 + tooltip_descriptions.keys
1.46 +
1.47 + private val gutter_elements =
1.48 + Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
1.49 +
1.50 + private val squiggly_elements =
1.51 + Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
1.52 +
1.53 + private val line_background_elements =
1.54 + Set(Markup.WRITELN_MESSAGE, Markup.TRACING_MESSAGE,
1.55 + Markup.WARNING_MESSAGE, Markup.ERROR_MESSAGE,
1.56 + Markup.INFORMATION)
1.57 +
1.58 + private val separator_elements = Set(Markup.SEPARATOR)
1.59 +
1.60 + private val background1_elements =
1.61 + Protocol.command_status_elements + Markup.WRITELN_MESSAGE +
1.62 + Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE +
1.63 + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY ++
1.64 + active_elements
1.65 +
1.66 + private val background2_elements = Set(Markup.TOKEN_RANGE)
1.67 +
1.68 + private val foreground_elements =
1.69 + Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
1.70 + Markup.CARTOUCHE, Markup.ANTIQUOTED)
1.71 +
1.72 + private val bullet_elements = Set(Markup.BULLET)
1.73 +
1.74 + private val fold_depth_elements =
1.75 + Set(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
1.76 }
1.77
1.78
1.79 @@ -202,14 +271,10 @@
1.80
1.81 /* completion context */
1.82
1.83 - private val completion_elements =
1.84 - Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.CARTOUCHE,
1.85 - Markup.COMMENT, Markup.LANGUAGE, Markup.ML_STRING, Markup.ML_COMMENT)
1.86 -
1.87 def completion_context(caret: Text.Offset): Option[Completion.Context] =
1.88 if (caret > 0) {
1.89 val result =
1.90 - snapshot.select_markup(Text.Range(caret - 1, caret + 1), completion_elements, _ =>
1.91 + snapshot.select_markup(Text.Range(caret - 1, caret + 1), Rendering.completion_elements, _ =>
1.92 {
1.93 case Text.Info(_, elem)
1.94 if elem.name == Markup.ML_STRING || elem.name == Markup.ML_COMMENT =>
1.95 @@ -229,7 +294,7 @@
1.96
1.97 /* command status overview */
1.98
1.99 - val overview_limit = options.int("jedit_text_overview_limit")
1.100 + def overview_limit: Int = options.int("jedit_text_overview_limit")
1.101
1.102 def overview_color(range: Text.Range): Option[Color] =
1.103 {
1.104 @@ -264,15 +329,9 @@
1.105
1.106 /* highlighted area */
1.107
1.108 - private val highlight_elements =
1.109 - Set(Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE,
1.110 - Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING,
1.111 - Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
1.112 - Markup.VAR, Markup.TFREE, Markup.TVAR)
1.113 -
1.114 def highlight(range: Text.Range): Option[Text.Info[Color]] =
1.115 {
1.116 - snapshot.select_markup(range, highlight_elements, _ =>
1.117 + snapshot.select_markup(range, Rendering.highlight_elements, _ =>
1.118 {
1.119 case info => Some(Text.Info(snapshot.convert(info.range), highlight_color))
1.120 }) match { case Text.Info(_, info) :: _ => Some(info) case _ => None }
1.121 @@ -281,9 +340,6 @@
1.122
1.123 /* hyperlinks */
1.124
1.125 - private val hyperlink_elements =
1.126 - Set(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL)
1.127 -
1.128 private def hyperlink_file(line: Int, name: String): Option[PIDE.editor.Hyperlink] =
1.129 if (Path.is_ok(name))
1.130 Isabelle_System.source_file(Path.explode(name)).map(path =>
1.131 @@ -301,7 +357,7 @@
1.132 def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
1.133 {
1.134 snapshot.cumulate_markup[Vector[Text.Info[PIDE.editor.Hyperlink]]](
1.135 - range, Vector.empty, hyperlink_elements, _ =>
1.136 + range, Vector.empty, Rendering.hyperlink_elements, _ =>
1.137 {
1.138 case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
1.139 if Path.is_ok(name) =>
1.140 @@ -343,11 +399,8 @@
1.141
1.142 /* active elements */
1.143
1.144 - private val active_elements =
1.145 - Set(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW, Markup.SENDBACK, Markup.SIMP_TRACE)
1.146 -
1.147 def active(range: Text.Range): Option[Text.Info[XML.Elem]] =
1.148 - snapshot.select_markup(range, active_elements, command_state =>
1.149 + snapshot.select_markup(range, Rendering.active_elements, command_state =>
1.150 {
1.151 case Text.Info(info_range, elem) =>
1.152 if (elem.name == Markup.DIALOG) {
1.153 @@ -373,14 +426,11 @@
1.154
1.155 /* tooltip messages */
1.156
1.157 - private val tooltip_message_elements =
1.158 - Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)
1.159 -
1.160 def tooltip_message(range: Text.Range): Option[Text.Info[XML.Body]] =
1.161 {
1.162 val results =
1.163 snapshot.cumulate_markup[List[Text.Info[Command.Results.Entry]]](
1.164 - range, Nil, tooltip_message_elements, _ =>
1.165 + range, Nil, Rendering.tooltip_message_elements, _ =>
1.166 {
1.167 case (msgs, Text.Info(info_range,
1.168 XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
1.169 @@ -407,25 +457,10 @@
1.170
1.171 /* tooltips */
1.172
1.173 - private val tooltips: Map[String, String] =
1.174 - Map(
1.175 - Markup.TOKEN_RANGE -> "inner syntax token",
1.176 - Markup.FREE -> "free variable",
1.177 - Markup.SKOLEM -> "skolem variable",
1.178 - Markup.BOUND -> "bound variable",
1.179 - Markup.VAR -> "schematic variable",
1.180 - Markup.TFREE -> "free type variable",
1.181 - Markup.TVAR -> "schematic type variable")
1.182 -
1.183 - private val tooltip_elements =
1.184 - Set(Markup.LANGUAGE, Markup.TIMING, Markup.ENTITY, Markup.SORTING,
1.185 - Markup.TYPING, Markup.ML_TYPING, Markup.PATH, Markup.URL) ++
1.186 - tooltips.keys
1.187 -
1.188 private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
1.189 Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)
1.190
1.191 - private val timing_threshold: Double = options.real("jedit_timing_threshold")
1.192 + private def timing_threshold: Double = options.real("jedit_timing_threshold")
1.193
1.194 def tooltip(range: Text.Range): Option[Text.Info[XML.Body]] =
1.195 {
1.196 @@ -441,7 +476,7 @@
1.197
1.198 val results =
1.199 snapshot.cumulate_markup[Text.Info[(Timing, Vector[(Boolean, XML.Tree)])]](
1.200 - range, Text.Info(range, (Timing.zero, Vector.empty)), tooltip_elements, _ =>
1.201 + range, Text.Info(range, (Timing.zero, Vector.empty)), Rendering.tooltip_elements, _ =>
1.202 {
1.203 case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
1.204 Some(Text.Info(r, (t1 + t2, info)))
1.205 @@ -468,9 +503,8 @@
1.206 case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _), _))) =>
1.207 Some(add(prev, r, (true, XML.Text("language: " + language))))
1.208 case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) =>
1.209 - if (tooltips.isDefinedAt(name))
1.210 - Some(add(prev, r, (true, XML.Text(tooltips(name)))))
1.211 - else None
1.212 + Rendering.tooltip_descriptions.get(name).
1.213 + map(descr => add(prev, r, (true, XML.Text(descr))))
1.214 }).map(_.info)
1.215
1.216 results.map(_.info).flatMap(res => res._2.toList) match {
1.217 @@ -482,7 +516,7 @@
1.218 }
1.219 }
1.220
1.221 - val tooltip_margin: Int = options.int("jedit_tooltip_margin")
1.222 + def tooltip_margin: Int = options.int("jedit_tooltip_margin")
1.223
1.224 lazy val tooltip_close_icon = JEdit_Lib.load_icon(options.string("tooltip_close_icon"))
1.225 lazy val tooltip_detach_icon = JEdit_Lib.load_icon(options.string("tooltip_detach_icon"))
1.226 @@ -496,13 +530,10 @@
1.227 Rendering.legacy_pri -> JEdit_Lib.load_icon(options.string("gutter_legacy_icon")),
1.228 Rendering.error_pri -> JEdit_Lib.load_icon(options.string("gutter_error_icon")))
1.229
1.230 - private val gutter_elements =
1.231 - Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
1.232 -
1.233 def gutter_message(range: Text.Range): Option[Icon] =
1.234 {
1.235 val results =
1.236 - snapshot.cumulate_markup[Int](range, 0, gutter_elements, _ =>
1.237 + snapshot.cumulate_markup[Int](range, 0, Rendering.gutter_elements, _ =>
1.238 {
1.239 case (pri, Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _),
1.240 List(XML.Elem(Markup(Markup.INFORMATION, _), _))))) =>
1.241 @@ -525,19 +556,16 @@
1.242
1.243 /* squiggly underline */
1.244
1.245 - private val squiggly_colors = Map(
1.246 + private lazy val squiggly_colors = Map(
1.247 Rendering.writeln_pri -> writeln_color,
1.248 Rendering.information_pri -> information_color,
1.249 Rendering.warning_pri -> warning_color,
1.250 Rendering.error_pri -> error_color)
1.251
1.252 - private val squiggly_elements =
1.253 - Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
1.254 -
1.255 def squiggly_underline(range: Text.Range): List[Text.Info[Color]] =
1.256 {
1.257 val results =
1.258 - snapshot.cumulate_markup[Int](range, 0, squiggly_elements, _ =>
1.259 + snapshot.cumulate_markup[Int](range, 0, Rendering.squiggly_elements, _ =>
1.260 {
1.261 case (pri, Text.Info(_, elem)) =>
1.262 if (Protocol.is_information(elem))
1.263 @@ -554,21 +582,17 @@
1.264
1.265 /* message output */
1.266
1.267 - private val message_colors = Map(
1.268 + private lazy val message_colors = Map(
1.269 Rendering.writeln_pri -> writeln_message_color,
1.270 Rendering.information_pri -> information_message_color,
1.271 Rendering.tracing_pri -> tracing_message_color,
1.272 Rendering.warning_pri -> warning_message_color,
1.273 Rendering.error_pri -> error_message_color)
1.274
1.275 - private val line_background_elements =
1.276 - Set(Markup.WRITELN_MESSAGE, Markup.TRACING_MESSAGE, Markup.WARNING_MESSAGE,
1.277 - Markup.ERROR_MESSAGE, Markup.INFORMATION)
1.278 -
1.279 def line_background(range: Text.Range): Option[(Color, Boolean)] =
1.280 {
1.281 val results =
1.282 - snapshot.cumulate_markup[Int](range, 0, line_background_elements, _ =>
1.283 + snapshot.cumulate_markup[Int](range, 0, Rendering.line_background_elements, _ =>
1.284 {
1.285 case (pri, Text.Info(_, elem)) =>
1.286 if (elem.name == Markup.INFORMATION)
1.287 @@ -580,7 +604,7 @@
1.288
1.289 val is_separator =
1.290 pri > 0 &&
1.291 - snapshot.cumulate_markup[Boolean](range, false, Set(Markup.SEPARATOR), _ =>
1.292 + snapshot.cumulate_markup[Boolean](range, false, Rendering.separator_elements, _ =>
1.293 {
1.294 case _ => Some(true)
1.295 }).exists(_.info)
1.296 @@ -594,11 +618,6 @@
1.297
1.298 /* text background */
1.299
1.300 - private val background1_elements =
1.301 - Protocol.command_status_elements + Markup.WRITELN_MESSAGE + Markup.TRACING_MESSAGE +
1.302 - Markup.WARNING_MESSAGE + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY ++
1.303 - active_elements
1.304 -
1.305 def background1(range: Text.Range): List[Text.Info[Color]] =
1.306 {
1.307 if (snapshot.is_outdated) List(Text.Info(range, outdated_color))
1.308 @@ -606,26 +625,27 @@
1.309 for {
1.310 Text.Info(r, result) <-
1.311 snapshot.cumulate_markup[(Option[Protocol.Status], Option[Color])](
1.312 - range, (Some(Protocol.Status.init), None), background1_elements, command_state =>
1.313 - {
1.314 - case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
1.315 - if (Protocol.command_status_elements(markup.name)) =>
1.316 - Some((Some(Protocol.command_status(status, markup)), color))
1.317 - case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
1.318 - Some((None, Some(bad_color)))
1.319 - case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
1.320 - Some((None, Some(intensify_color)))
1.321 - case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
1.322 - command_state.results.get(serial) match {
1.323 - case Some(Protocol.Dialog_Result(res)) if res == result =>
1.324 - Some((None, Some(active_result_color)))
1.325 - case _ =>
1.326 - Some((None, Some(active_color)))
1.327 - }
1.328 - case (_, Text.Info(_, elem)) =>
1.329 - if (active_elements(elem.name)) Some((None, Some(active_color)))
1.330 - else None
1.331 - })
1.332 + range, (Some(Protocol.Status.init), None), Rendering.background1_elements,
1.333 + command_state =>
1.334 + {
1.335 + case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
1.336 + if (Protocol.command_status_elements(markup.name)) =>
1.337 + Some((Some(Protocol.command_status(status, markup)), color))
1.338 + case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
1.339 + Some((None, Some(bad_color)))
1.340 + case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
1.341 + Some((None, Some(intensify_color)))
1.342 + case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
1.343 + command_state.results.get(serial) match {
1.344 + case Some(Protocol.Dialog_Result(res)) if res == result =>
1.345 + Some((None, Some(active_result_color)))
1.346 + case _ =>
1.347 + Some((None, Some(active_color)))
1.348 + }
1.349 + case (_, Text.Info(_, elem)) =>
1.350 + if (Rendering.active_elements(elem.name)) Some((None, Some(active_color)))
1.351 + else None
1.352 + })
1.353 color <-
1.354 (result match {
1.355 case (Some(status), opt_color) =>
1.356 @@ -638,16 +658,13 @@
1.357 }
1.358
1.359 def background2(range: Text.Range): List[Text.Info[Color]] =
1.360 - snapshot.select_markup(range, Set(Markup.TOKEN_RANGE), _ => _ => Some(light_color))
1.361 + snapshot.select_markup(range, Rendering.background2_elements, _ => _ => Some(light_color))
1.362
1.363
1.364 /* text foreground */
1.365
1.366 - private val foreground_elements =
1.367 - Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.CARTOUCHE, Markup.ANTIQUOTED)
1.368 -
1.369 def foreground(range: Text.Range): List[Text.Info[Color]] =
1.370 - snapshot.select_markup(range, foreground_elements, _ =>
1.371 + snapshot.select_markup(range, Rendering.foreground_elements, _ =>
1.372 {
1.373 case Text.Info(_, elem) =>
1.374 if (elem.name == Markup.ANTIQUOTED) Some(antiquoted_color) else Some(quoted_color)
1.375 @@ -656,7 +673,7 @@
1.376
1.377 /* text color */
1.378
1.379 - private val text_colors: Map[String, Color] = Map(
1.380 + private lazy val text_colors: Map[String, Color] = Map(
1.381 Markup.KEYWORD1 -> keyword1_color,
1.382 Markup.KEYWORD2 -> keyword2_color,
1.383 Markup.STRING -> Color.BLACK,
1.384 @@ -685,7 +702,7 @@
1.385 Markup.ML_STRING -> inner_quoted_color,
1.386 Markup.ML_COMMENT -> inner_comment_color)
1.387
1.388 - private val text_color_elements = text_colors.keySet
1.389 + private lazy val text_color_elements = text_colors.keySet
1.390
1.391 def text_color(range: Text.Range, color: Color): List[Text.Info[Color]] =
1.392 {
1.393 @@ -701,16 +718,13 @@
1.394 /* virtual bullets */
1.395
1.396 def bullet(range: Text.Range): List[Text.Info[Color]] =
1.397 - snapshot.select_markup(range, Set(Markup.BULLET), _ => _ => Some(bullet_color))
1.398 + snapshot.select_markup(range, Rendering.bullet_elements, _ => _ => Some(bullet_color))
1.399
1.400
1.401 /* text folds */
1.402
1.403 - private val fold_depth_elements =
1.404 - Set(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
1.405 -
1.406 def fold_depth(range: Text.Range): List[Text.Info[Int]] =
1.407 - snapshot.cumulate_markup[Int](range, 0, fold_depth_elements, _ =>
1.408 + snapshot.cumulate_markup[Int](range, 0, Rendering.fold_depth_elements, _ =>
1.409 {
1.410 case (depth, _) => Some(depth + 1)
1.411 })