# HG changeset patch # User wenzelm # Date 1375877639 -7200 # Node ID 36e2c0c308eb258d3ae4762375d443b2bdb46093 # Parent ea3338812e67622fc76caf519939c48d8b62e27e tuned signature; tuned; diff -r ea3338812e67 -r 36e2c0c308eb src/Pure/PIDE/xml.scala --- a/src/Pure/PIDE/xml.scala Wed Aug 07 13:46:32 2013 +0200 +++ b/src/Pure/PIDE/xml.scala Wed Aug 07 14:13:59 2013 +0200 @@ -22,6 +22,9 @@ sealed abstract class Tree { override def toString = string_of_tree(this) } case class Elem(markup: Markup, body: List[Tree]) extends Tree + { + def name: String = markup.name + } case class Text(content: String) extends Tree def elem(name: String, body: List[Tree]) = Elem(Markup(name, Nil), body) diff -r ea3338812e67 -r 36e2c0c308eb src/Tools/jEdit/src/query_operation.scala --- a/src/Tools/jEdit/src/query_operation.scala Wed Aug 07 13:46:32 2013 +0200 +++ b/src/Tools/jEdit/src/query_operation.scala Wed Aug 07 14:13:59 2013 +0200 @@ -141,7 +141,7 @@ /* status */ def get_status(name: String, status: Status.Value): Option[Status.Value] = - results.collectFirst({ case List(XML.Elem(m, _)) if m.name == name => status }) + results.collectFirst({ case List(elem: XML.Elem) if elem.name == name => status }) val new_status = get_status(Markup.FINISHED, Status.FINISHED) orElse diff -r ea3338812e67 -r 36e2c0c308eb src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Wed Aug 07 13:46:32 2013 +0200 +++ b/src/Tools/jEdit/src/rendering.scala Wed Aug 07 14:13:59 2013 +0200 @@ -154,11 +154,11 @@ snapshot.cumulate_markup[(Protocol.Status, Int)]( range, (Protocol.Status.init, 0), Some(overview_include), _ => { - case ((status, pri), Text.Info(_, XML.Elem(markup, _))) => - if (markup.name == Markup.WARNING || markup.name == Markup.ERROR) - Some((status, pri max Rendering.message_pri(markup.name))) - else if (overview_include(markup.name)) - Some((Protocol.command_status(status, markup), pri)) + case ((status, pri), Text.Info(_, elem)) => + if (elem.name == Markup.WARNING || elem.name == Markup.ERROR) + Some((status, pri max Rendering.message_pri(elem.name))) + else if (overview_include(elem.name)) + Some((Protocol.command_status(status, elem.markup), pri)) else None }) if (results.isEmpty) None @@ -189,8 +189,8 @@ { snapshot.select_markup(range, Some(highlight_include), _ => { - case Text.Info(info_range, XML.Elem(markup, _)) => - if (highlight_include(markup.name)) + case Text.Info(info_range, elem) => + if (highlight_include(elem.name)) Some(Text.Info(snapshot.convert(info_range), highlight_color)) else None }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None } @@ -257,8 +257,10 @@ case Text.Info(info_range, elem @ Protocol.Dialog(_, serial, _)) if !command_state.results.defined(serial) => Some(Text.Info(snapshot.convert(info_range), elem)) - case Text.Info(info_range, elem @ XML.Elem(Markup(name, _), _)) => - if (name == Markup.BROWSER || name == Markup.GRAPHVIEW || name == Markup.SENDBACK) + case Text.Info(info_range, elem) => + if (elem.name == Markup.BROWSER || + elem.name == Markup.GRAPHVIEW || + elem.name == Markup.SENDBACK) Some(Text.Info(snapshot.convert(info_range), elem)) else None }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None } @@ -427,11 +429,11 @@ val results = snapshot.cumulate_markup[Int](range, 0, Some(squiggly_include), _ => { - case (pri, Text.Info(_, msg @ XML.Elem(markup, _))) => - if (Protocol.is_information(msg)) + case (pri, Text.Info(_, elem)) => + if (Protocol.is_information(elem)) Some(pri max Rendering.information_pri) - else if (squiggly_include.contains(markup.name)) - Some(pri max Rendering.message_pri(markup.name)) + else if (squiggly_include.contains(elem.name)) + Some(pri max Rendering.message_pri(elem.name)) else None }) for { @@ -457,11 +459,12 @@ val results = snapshot.cumulate_markup[Int](range, 0, Some(line_background_elements), _ => { - case (pri, Text.Info(_, XML.Elem(Markup(Markup.INFORMATION, _), _))) => - Some(pri max Rendering.information_pri) - case (pri, Text.Info(_, XML.Elem(Markup(name, _), _))) => - if (name == Markup.WRITELN_MESSAGE || name == Markup.TRACING_MESSAGE || - name == Markup.WARNING_MESSAGE || name == Markup.ERROR_MESSAGE) + case (pri, Text.Info(_, elem)) => + val name = elem.name + if (name == Markup.INFORMATION) + Some(pri max Rendering.information_pri) + else if (name == Markup.WRITELN_MESSAGE || name == Markup.TRACING_MESSAGE || + elem.name == Markup.WARNING_MESSAGE || name == Markup.ERROR_MESSAGE) Some(pri max Rendering.message_pri(name)) else None }) @@ -470,8 +473,8 @@ val is_separator = pri > 0 && snapshot.cumulate_markup[Boolean](range, false, Some(Set(Markup.SEPARATOR)), _ => { - case (_, Text.Info(_, XML.Elem(Markup(Markup.SEPARATOR, _), _))) => Some(true) - case _ => None + case (_, Text.Info(_, elem)) => + if (elem.name == Markup.SEPARATOR) Some(true) else None }).exists(_.info) message_colors.get(pri).map((_, is_separator)) @@ -512,8 +515,8 @@ case _ => Some((None, Some(active_color))) } - case (_, Text.Info(_, XML.Elem(markup, _))) => - if (active_include(markup.name)) Some((None, Some(active_color))) + case (_, Text.Info(_, elem)) => + if (active_include(elem.name)) Some((None, Some(active_color))) else None }) color <- @@ -531,30 +534,29 @@ def background2(range: Text.Range): Stream[Text.Info[Color]] = snapshot.select_markup(range, Some(Set(Markup.TOKEN_RANGE)), _ => { - case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => Some(light_color) - case _ => None + case Text.Info(_, elem) => + if (elem.name == Markup.TOKEN_RANGE) Some(light_color) else None }) def bullet(range: Text.Range): Stream[Text.Info[Color]] = snapshot.select_markup(range, Some(Set(Markup.BULLET)), _ => { - case Text.Info(_, XML.Elem(Markup(Markup.BULLET, _), _)) => Some(bullet_color) - case _ => None + case Text.Info(_, elem) => + if (elem.name == Markup.BULLET) Some(bullet_color) else None }) - private val foreground_elements = + private val foreground_include = Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.ANTIQ) def foreground(range: Text.Range): Stream[Text.Info[Color]] = - snapshot.select_markup(range, Some(foreground_elements), _ => + snapshot.select_markup(range, Some(foreground_include), _ => { - case Text.Info(_, XML.Elem(Markup(Markup.STRING, _), _)) => Some(quoted_color) - case Text.Info(_, XML.Elem(Markup(Markup.ALTSTRING, _), _)) => Some(quoted_color) - case Text.Info(_, XML.Elem(Markup(Markup.VERBATIM, _), _)) => Some(quoted_color) - case Text.Info(_, XML.Elem(Markup(Markup.ANTIQ, _), _)) => Some(antiquoted_color) - case _ => None + case Text.Info(_, elem) => + if (elem.name == Markup.ANTIQ) Some(antiquoted_color) + else if (foreground_include.contains(elem.name)) Some(quoted_color) + else None }) @@ -591,7 +593,7 @@ else snapshot.cumulate_markup(range, color, Some(text_color_elements), _ => { - case (_, Text.Info(_, XML.Elem(markup, _))) => text_colors.get(markup.name) + case (_, Text.Info(_, elem)) => text_colors.get(elem.name) }) } @@ -603,7 +605,7 @@ def fold_depth(range: Text.Range): Stream[Text.Info[Int]] = snapshot.cumulate_markup[Int](range, 0, Some(fold_depth_include), _ => { - case (depth, Text.Info(_, XML.Elem(markup, _))) => - if (fold_depth_include(markup.name)) Some(depth + 1) else None + case (depth, Text.Info(_, elem)) => + if (fold_depth_include(elem.name)) Some(depth + 1) else None }) }