tuned signature;
authorwenzelm
Wed Aug 07 14:13:59 2013 +0200 (2013-08-07 ago)
changeset 5289036e2c0c308eb
parent 52889 ea3338812e67
child 52891 b8dede3a4f1d
tuned signature;
tuned;
src/Pure/PIDE/xml.scala
src/Tools/jEdit/src/query_operation.scala
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Pure/PIDE/xml.scala	Wed Aug 07 13:46:32 2013 +0200
     1.2 +++ b/src/Pure/PIDE/xml.scala	Wed Aug 07 14:13:59 2013 +0200
     1.3 @@ -22,6 +22,9 @@
     1.4  
     1.5    sealed abstract class Tree { override def toString = string_of_tree(this) }
     1.6    case class Elem(markup: Markup, body: List[Tree]) extends Tree
     1.7 +  {
     1.8 +    def name: String = markup.name
     1.9 +  }
    1.10    case class Text(content: String) extends Tree
    1.11  
    1.12    def elem(name: String, body: List[Tree]) = Elem(Markup(name, Nil), body)
     2.1 --- a/src/Tools/jEdit/src/query_operation.scala	Wed Aug 07 13:46:32 2013 +0200
     2.2 +++ b/src/Tools/jEdit/src/query_operation.scala	Wed Aug 07 14:13:59 2013 +0200
     2.3 @@ -141,7 +141,7 @@
     2.4      /* status */
     2.5  
     2.6      def get_status(name: String, status: Status.Value): Option[Status.Value] =
     2.7 -      results.collectFirst({ case List(XML.Elem(m, _)) if m.name == name => status })
     2.8 +      results.collectFirst({ case List(elem: XML.Elem) if elem.name == name => status })
     2.9  
    2.10      val new_status =
    2.11        get_status(Markup.FINISHED, Status.FINISHED) orElse
     3.1 --- a/src/Tools/jEdit/src/rendering.scala	Wed Aug 07 13:46:32 2013 +0200
     3.2 +++ b/src/Tools/jEdit/src/rendering.scala	Wed Aug 07 14:13:59 2013 +0200
     3.3 @@ -154,11 +154,11 @@
     3.4          snapshot.cumulate_markup[(Protocol.Status, Int)](
     3.5            range, (Protocol.Status.init, 0), Some(overview_include), _ =>
     3.6            {
     3.7 -            case ((status, pri), Text.Info(_, XML.Elem(markup, _))) =>
     3.8 -              if (markup.name == Markup.WARNING || markup.name == Markup.ERROR)
     3.9 -                Some((status, pri max Rendering.message_pri(markup.name)))
    3.10 -              else if (overview_include(markup.name))
    3.11 -                Some((Protocol.command_status(status, markup), pri))
    3.12 +            case ((status, pri), Text.Info(_, elem)) =>
    3.13 +              if (elem.name == Markup.WARNING || elem.name == Markup.ERROR)
    3.14 +                Some((status, pri max Rendering.message_pri(elem.name)))
    3.15 +              else if (overview_include(elem.name))
    3.16 +                Some((Protocol.command_status(status, elem.markup), pri))
    3.17                else None
    3.18            })
    3.19        if (results.isEmpty) None
    3.20 @@ -189,8 +189,8 @@
    3.21    {
    3.22      snapshot.select_markup(range, Some(highlight_include), _ =>
    3.23          {
    3.24 -          case Text.Info(info_range, XML.Elem(markup, _)) =>
    3.25 -            if (highlight_include(markup.name))
    3.26 +          case Text.Info(info_range, elem) =>
    3.27 +            if (highlight_include(elem.name))
    3.28                Some(Text.Info(snapshot.convert(info_range), highlight_color))
    3.29              else None
    3.30          }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
    3.31 @@ -257,8 +257,10 @@
    3.32            case Text.Info(info_range, elem @ Protocol.Dialog(_, serial, _))
    3.33            if !command_state.results.defined(serial) =>
    3.34              Some(Text.Info(snapshot.convert(info_range), elem))
    3.35 -          case Text.Info(info_range, elem @ XML.Elem(Markup(name, _), _)) =>
    3.36 -            if (name == Markup.BROWSER || name == Markup.GRAPHVIEW || name == Markup.SENDBACK)
    3.37 +          case Text.Info(info_range, elem) =>
    3.38 +            if (elem.name == Markup.BROWSER ||
    3.39 +                elem.name == Markup.GRAPHVIEW ||
    3.40 +                elem.name == Markup.SENDBACK)
    3.41                Some(Text.Info(snapshot.convert(info_range), elem))
    3.42              else None
    3.43          }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
    3.44 @@ -427,11 +429,11 @@
    3.45      val results =
    3.46        snapshot.cumulate_markup[Int](range, 0, Some(squiggly_include), _ =>
    3.47          {
    3.48 -          case (pri, Text.Info(_, msg @ XML.Elem(markup, _))) =>
    3.49 -            if (Protocol.is_information(msg))
    3.50 +          case (pri, Text.Info(_, elem)) =>
    3.51 +            if (Protocol.is_information(elem))
    3.52                Some(pri max Rendering.information_pri)
    3.53 -            else if (squiggly_include.contains(markup.name))
    3.54 -              Some(pri max Rendering.message_pri(markup.name))
    3.55 +            else if (squiggly_include.contains(elem.name))
    3.56 +              Some(pri max Rendering.message_pri(elem.name))
    3.57              else None
    3.58          })
    3.59      for {
    3.60 @@ -457,11 +459,12 @@
    3.61      val results =
    3.62        snapshot.cumulate_markup[Int](range, 0, Some(line_background_elements), _ =>
    3.63          {
    3.64 -          case (pri, Text.Info(_, XML.Elem(Markup(Markup.INFORMATION, _), _))) =>
    3.65 -            Some(pri max Rendering.information_pri)
    3.66 -          case (pri, Text.Info(_, XML.Elem(Markup(name, _), _))) =>
    3.67 -            if (name == Markup.WRITELN_MESSAGE || name == Markup.TRACING_MESSAGE ||
    3.68 -                name == Markup.WARNING_MESSAGE || name == Markup.ERROR_MESSAGE)
    3.69 +          case (pri, Text.Info(_, elem)) =>
    3.70 +            val name = elem.name
    3.71 +            if (name == Markup.INFORMATION)
    3.72 +              Some(pri max Rendering.information_pri)
    3.73 +            else if (name == Markup.WRITELN_MESSAGE || name == Markup.TRACING_MESSAGE ||
    3.74 +                elem.name == Markup.WARNING_MESSAGE || name == Markup.ERROR_MESSAGE)
    3.75                Some(pri max Rendering.message_pri(name))
    3.76              else None
    3.77          })
    3.78 @@ -470,8 +473,8 @@
    3.79      val is_separator = pri > 0 &&
    3.80        snapshot.cumulate_markup[Boolean](range, false, Some(Set(Markup.SEPARATOR)), _ =>
    3.81          {
    3.82 -          case (_, Text.Info(_, XML.Elem(Markup(Markup.SEPARATOR, _), _))) => Some(true)
    3.83 -          case _ => None
    3.84 +          case (_, Text.Info(_, elem)) =>
    3.85 +            if (elem.name == Markup.SEPARATOR) Some(true) else None
    3.86          }).exists(_.info)
    3.87  
    3.88      message_colors.get(pri).map((_, is_separator))
    3.89 @@ -512,8 +515,8 @@
    3.90                    case _ =>
    3.91                      Some((None, Some(active_color)))
    3.92                  }
    3.93 -              case (_, Text.Info(_, XML.Elem(markup, _))) =>
    3.94 -                if (active_include(markup.name)) Some((None, Some(active_color)))
    3.95 +              case (_, Text.Info(_, elem)) =>
    3.96 +                if (active_include(elem.name)) Some((None, Some(active_color)))
    3.97                  else None
    3.98              })
    3.99          color <-
   3.100 @@ -531,30 +534,29 @@
   3.101    def background2(range: Text.Range): Stream[Text.Info[Color]] =
   3.102      snapshot.select_markup(range, Some(Set(Markup.TOKEN_RANGE)), _ =>
   3.103        {
   3.104 -        case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => Some(light_color)
   3.105 -        case _ => None
   3.106 +        case Text.Info(_, elem) =>
   3.107 +          if (elem.name == Markup.TOKEN_RANGE) Some(light_color) else None
   3.108        })
   3.109  
   3.110  
   3.111    def bullet(range: Text.Range): Stream[Text.Info[Color]] =
   3.112      snapshot.select_markup(range, Some(Set(Markup.BULLET)), _ =>
   3.113        {
   3.114 -        case Text.Info(_, XML.Elem(Markup(Markup.BULLET, _), _)) => Some(bullet_color)
   3.115 -        case _ => None
   3.116 +        case Text.Info(_, elem) =>
   3.117 +          if (elem.name == Markup.BULLET) Some(bullet_color) else None
   3.118        })
   3.119  
   3.120  
   3.121 -  private val foreground_elements =
   3.122 +  private val foreground_include =
   3.123      Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.ANTIQ)
   3.124  
   3.125    def foreground(range: Text.Range): Stream[Text.Info[Color]] =
   3.126 -    snapshot.select_markup(range, Some(foreground_elements), _ =>
   3.127 +    snapshot.select_markup(range, Some(foreground_include), _ =>
   3.128        {
   3.129 -        case Text.Info(_, XML.Elem(Markup(Markup.STRING, _), _)) => Some(quoted_color)
   3.130 -        case Text.Info(_, XML.Elem(Markup(Markup.ALTSTRING, _), _)) => Some(quoted_color)
   3.131 -        case Text.Info(_, XML.Elem(Markup(Markup.VERBATIM, _), _)) => Some(quoted_color)
   3.132 -        case Text.Info(_, XML.Elem(Markup(Markup.ANTIQ, _), _)) => Some(antiquoted_color)
   3.133 -        case _ => None
   3.134 +        case Text.Info(_, elem) =>
   3.135 +          if (elem.name == Markup.ANTIQ) Some(antiquoted_color)
   3.136 +          else if (foreground_include.contains(elem.name)) Some(quoted_color)
   3.137 +          else None
   3.138        })
   3.139  
   3.140  
   3.141 @@ -591,7 +593,7 @@
   3.142      else
   3.143        snapshot.cumulate_markup(range, color, Some(text_color_elements), _ =>
   3.144          {
   3.145 -          case (_, Text.Info(_, XML.Elem(markup, _))) => text_colors.get(markup.name)
   3.146 +          case (_, Text.Info(_, elem)) => text_colors.get(elem.name)
   3.147          })
   3.148    }
   3.149  
   3.150 @@ -603,7 +605,7 @@
   3.151    def fold_depth(range: Text.Range): Stream[Text.Info[Int]] =
   3.152      snapshot.cumulate_markup[Int](range, 0, Some(fold_depth_include), _ =>
   3.153        {
   3.154 -        case (depth, Text.Info(_, XML.Elem(markup, _))) =>
   3.155 -          if (fold_depth_include(markup.name)) Some(depth + 1) else None
   3.156 +        case (depth, Text.Info(_, elem)) =>
   3.157 +          if (fold_depth_include(elem.name)) Some(depth + 1) else None
   3.158        })
   3.159  }