src/Tools/jEdit/src/rendering.scala
changeset 55620 19dffae33cde
parent 55619 c5aeeacdd2b1
child 55622 ce575c2212fc
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Thu Feb 20 15:15:41 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Thu Feb 20 16:00:37 2014 +0100
     1.3 @@ -209,14 +209,12 @@
     1.4    def completion_context(caret: Text.Offset): Option[Completion.Context] =
     1.5      if (caret > 0) {
     1.6        val result =
     1.7 -        snapshot.select_markup(Text.Range(caret - 1, caret + 1), Some(completion_elements), _ =>
     1.8 +        snapshot.select_markup(Text.Range(caret - 1, caret + 1), completion_elements, _ =>
     1.9            {
    1.10              case Text.Info(_, XML.Elem(Markup.Language(language, symbols), _)) =>
    1.11                Some(Completion.Context(language, symbols))
    1.12              case Text.Info(_, XML.Elem(markup, _)) =>
    1.13 -              if (completion_elements(markup.name))
    1.14 -                Some(Completion.Context(Markup.Language.UNKNOWN, true))
    1.15 -              else None
    1.16 +              Some(Completion.Context(Markup.Language.UNKNOWN, true))
    1.17            })
    1.18        result match {
    1.19          case Text.Info(_, context) :: _ => Some(context)
    1.20 @@ -239,14 +237,13 @@
    1.21      else {
    1.22        val results =
    1.23          snapshot.cumulate_markup[(Protocol.Status, Int)](
    1.24 -          range, (Protocol.Status.init, 0), Some(overview_elements), _ =>
    1.25 +          range, (Protocol.Status.init, 0), overview_elements, _ =>
    1.26            {
    1.27              case ((status, pri), Text.Info(_, elem)) =>
    1.28                if (elem.name == Markup.WARNING || elem.name == Markup.ERROR)
    1.29                  Some((status, pri max Rendering.message_pri(elem.name)))
    1.30 -              else if (overview_elements(elem.name))
    1.31 +              else
    1.32                  Some((Protocol.command_status(status, elem.markup), pri))
    1.33 -              else None
    1.34            })
    1.35        if (results.isEmpty) None
    1.36        else {
    1.37 @@ -275,13 +272,10 @@
    1.38  
    1.39    def highlight(range: Text.Range): Option[Text.Info[Color]] =
    1.40    {
    1.41 -    snapshot.select_markup(range, Some(highlight_elements), _ =>
    1.42 -        {
    1.43 -          case Text.Info(info_range, elem) =>
    1.44 -            if (highlight_elements(elem.name))
    1.45 -              Some(Text.Info(snapshot.convert(info_range), highlight_color))
    1.46 -            else None
    1.47 -        }) match { case Text.Info(_, info) :: _ => Some(info) case _ => None }
    1.48 +    snapshot.select_markup(range, highlight_elements, _ =>
    1.49 +      {
    1.50 +        case info => Some(Text.Info(snapshot.convert(info.range), highlight_color))
    1.51 +      }) match { case Text.Info(_, info) :: _ => Some(info) case _ => None }
    1.52    }
    1.53  
    1.54  
    1.55 @@ -305,7 +299,7 @@
    1.56    def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
    1.57    {
    1.58      snapshot.cumulate_markup[List[Text.Info[PIDE.editor.Hyperlink]]](
    1.59 -      range, Nil, Some(hyperlink_elements), _ =>
    1.60 +      range, Nil, hyperlink_elements, _ =>
    1.61          {
    1.62            case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
    1.63            if Path.is_ok(name) =>
    1.64 @@ -349,34 +343,37 @@
    1.65      Set(Markup.BROWSER, Markup.GRAPHVIEW, Markup.SENDBACK, Markup.DIALOG, Markup.SIMP_TRACE)
    1.66  
    1.67    def active(range: Text.Range): Option[Text.Info[XML.Elem]] =
    1.68 -    snapshot.select_markup(range, Some(active_elements), command_state =>
    1.69 -        {
    1.70 -          case Text.Info(info_range, elem @ Protocol.Dialog(_, serial, _))
    1.71 -          if !command_state.results.defined(serial) =>
    1.72 +    snapshot.select_markup(range, active_elements, command_state =>
    1.73 +      {
    1.74 +        case Text.Info(info_range, elem @ Protocol.Dialog(_, serial, _))
    1.75 +        if !command_state.results.defined(serial) =>
    1.76 +          Some(Text.Info(snapshot.convert(info_range), elem))
    1.77 +        case Text.Info(info_range, elem) =>
    1.78 +          if (elem.name == Markup.BROWSER ||
    1.79 +              elem.name == Markup.GRAPHVIEW ||
    1.80 +              elem.name == Markup.SENDBACK ||
    1.81 +              elem.name == Markup.SIMP_TRACE)
    1.82              Some(Text.Info(snapshot.convert(info_range), elem))
    1.83 -          case Text.Info(info_range, elem) =>
    1.84 -            if (elem.name == Markup.BROWSER ||
    1.85 -                elem.name == Markup.GRAPHVIEW ||
    1.86 -                elem.name == Markup.SENDBACK ||
    1.87 -                elem.name == Markup.SIMP_TRACE)
    1.88 -              Some(Text.Info(snapshot.convert(info_range), elem))
    1.89 -            else None
    1.90 -        }) match { case Text.Info(_, info) :: _ => Some(info) case _ => None }
    1.91 +          else None
    1.92 +      }) match { case Text.Info(_, info) :: _ => Some(info) case _ => None }
    1.93  
    1.94  
    1.95    def command_results(range: Text.Range): Command.Results =
    1.96    {
    1.97      val results =
    1.98 -      snapshot.select_markup[Command.Results](range, None, command_state =>
    1.99 +      snapshot.select_markup[Command.Results](range, _ => true, command_state =>
   1.100          { case _ => Some(command_state.results) }).map(_.info)
   1.101      (Command.Results.empty /: results)(_ ++ _)
   1.102    }
   1.103  
   1.104 +  private val tooltip_message_elements =
   1.105 +    Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)
   1.106 +
   1.107    def tooltip_message(range: Text.Range): Option[Text.Info[XML.Body]] =
   1.108    {
   1.109      val results =
   1.110 -      snapshot.cumulate_markup[List[Text.Info[Command.Results.Entry]]](range, Nil,
   1.111 -        Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)), _ =>
   1.112 +      snapshot.cumulate_markup[List[Text.Info[Command.Results.Entry]]](
   1.113 +        range, Nil, tooltip_message_elements, _ =>
   1.114          {
   1.115            case (msgs, Text.Info(info_range,
   1.116              XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
   1.117 @@ -433,7 +430,7 @@
   1.118  
   1.119      val results =
   1.120        snapshot.cumulate_markup[Text.Info[(Timing, List[(Boolean, XML.Tree)])]](
   1.121 -        range, Text.Info(range, (Timing.zero, Nil)), Some(tooltip_elements), _ =>
   1.122 +        range, Text.Info(range, (Timing.zero, Nil)), tooltip_elements, _ =>
   1.123          {
   1.124            case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
   1.125              Some(Text.Info(r, (t1 + t2, info)))
   1.126 @@ -486,12 +483,13 @@
   1.127      Rendering.legacy_pri -> JEdit_Lib.load_icon(options.string("gutter_legacy_icon")),
   1.128      Rendering.error_pri -> JEdit_Lib.load_icon(options.string("gutter_error_icon")))
   1.129  
   1.130 -  private val gutter_elements = Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
   1.131 +  private val gutter_elements =
   1.132 +    Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
   1.133  
   1.134    def gutter_message(range: Text.Range): Option[Icon] =
   1.135    {
   1.136      val results =
   1.137 -      snapshot.cumulate_markup[Int](range, 0, Some(gutter_elements), _ =>
   1.138 +      snapshot.cumulate_markup[Int](range, 0, gutter_elements, _ =>
   1.139          {
   1.140            case (pri, Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _),
   1.141                List(XML.Elem(Markup(Markup.INFORMATION, _), _))))) =>
   1.142 @@ -523,14 +521,13 @@
   1.143    def squiggly_underline(range: Text.Range): List[Text.Info[Color]] =
   1.144    {
   1.145      val results =
   1.146 -      snapshot.cumulate_markup[Int](range, 0, Some(squiggly_elements), _ =>
   1.147 +      snapshot.cumulate_markup[Int](range, 0, squiggly_elements, _ =>
   1.148          {
   1.149            case (pri, Text.Info(_, elem)) =>
   1.150              if (Protocol.is_information(elem))
   1.151                Some(pri max Rendering.information_pri)
   1.152 -            else if (squiggly_elements(elem.name))
   1.153 +            else
   1.154                Some(pri max Rendering.message_pri(elem.name))
   1.155 -            else None
   1.156          })
   1.157      for {
   1.158        Text.Info(r, pri) <- results
   1.159 @@ -553,7 +550,7 @@
   1.160    def line_background(range: Text.Range): Option[(Color, Boolean)] =
   1.161    {
   1.162      val results =
   1.163 -      snapshot.cumulate_markup[Int](range, 0, Some(line_background_elements), _ =>
   1.164 +      snapshot.cumulate_markup[Int](range, 0, line_background_elements, _ =>
   1.165          {
   1.166            case (pri, Text.Info(_, elem)) =>
   1.167              val name = elem.name
   1.168 @@ -567,7 +564,7 @@
   1.169      val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
   1.170  
   1.171      val is_separator = pri > 0 &&
   1.172 -      snapshot.cumulate_markup[Boolean](range, false, Some(Set(Markup.SEPARATOR)), _ =>
   1.173 +      snapshot.cumulate_markup[Boolean](range, false, Set(Markup.SEPARATOR), _ =>
   1.174          {
   1.175            case (_, Text.Info(_, elem)) =>
   1.176              if (elem.name == Markup.SEPARATOR) Some(true) else None
   1.177 @@ -593,7 +590,7 @@
   1.178        for {
   1.179          Text.Info(r, result) <-
   1.180            snapshot.cumulate_markup[(Option[Protocol.Status], Option[Color])](
   1.181 -            range, (Some(Protocol.Status.init), None), Some(background1_elements), command_state =>
   1.182 +            range, (Some(Protocol.Status.init), None), background1_elements, command_state =>
   1.183              {
   1.184                case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
   1.185                if (Protocol.command_status_markup(markup.name)) =>
   1.186 @@ -626,7 +623,7 @@
   1.187  
   1.188  
   1.189    def background2(range: Text.Range): List[Text.Info[Color]] =
   1.190 -    snapshot.select_markup(range, Some(Set(Markup.TOKEN_RANGE)), _ =>
   1.191 +    snapshot.select_markup(range, Set(Markup.TOKEN_RANGE), _ =>
   1.192        {
   1.193          case Text.Info(_, elem) =>
   1.194            if (elem.name == Markup.TOKEN_RANGE) Some(light_color) else None
   1.195 @@ -634,7 +631,7 @@
   1.196  
   1.197  
   1.198    def bullet(range: Text.Range): List[Text.Info[Color]] =
   1.199 -    snapshot.select_markup(range, Some(Set(Markup.BULLET)), _ =>
   1.200 +    snapshot.select_markup(range, Set(Markup.BULLET), _ =>
   1.201        {
   1.202          case Text.Info(_, elem) =>
   1.203            if (elem.name == Markup.BULLET) Some(bullet_color) else None
   1.204 @@ -645,12 +642,10 @@
   1.205      Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.CARTOUCHE, Markup.ANTIQUOTED)
   1.206  
   1.207    def foreground(range: Text.Range): List[Text.Info[Color]] =
   1.208 -    snapshot.select_markup(range, Some(foreground_elements), _ =>
   1.209 +    snapshot.select_markup(range, foreground_elements, _ =>
   1.210        {
   1.211          case Text.Info(_, elem) =>
   1.212 -          if (elem.name == Markup.ANTIQUOTED) Some(antiquoted_color)
   1.213 -          else if (foreground_elements(elem.name)) Some(quoted_color)
   1.214 -          else None
   1.215 +          if (elem.name == Markup.ANTIQUOTED) Some(antiquoted_color) else Some(quoted_color)
   1.216        })
   1.217  
   1.218  
   1.219 @@ -689,7 +684,7 @@
   1.220    {
   1.221      if (color == Token_Markup.hidden_color) List(Text.Info(range, color))
   1.222      else
   1.223 -      snapshot.cumulate_markup(range, color, Some(text_color_elements), _ =>
   1.224 +      snapshot.cumulate_markup(range, color, text_color_elements, _ =>
   1.225          {
   1.226            case (_, Text.Info(_, elem)) => text_colors.get(elem.name)
   1.227          })
   1.228 @@ -698,12 +693,12 @@
   1.229  
   1.230    /* nested text structure -- folds */
   1.231  
   1.232 -  private val fold_depth_elements = Set(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
   1.233 +  private val fold_depth_elements =
   1.234 +    Set(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
   1.235  
   1.236    def fold_depth(range: Text.Range): List[Text.Info[Int]] =
   1.237 -    snapshot.cumulate_markup[Int](range, 0, Some(fold_depth_elements), _ =>
   1.238 +    snapshot.cumulate_markup[Int](range, 0, fold_depth_elements, _ =>
   1.239        {
   1.240 -        case (depth, Text.Info(_, elem)) =>
   1.241 -          if (fold_depth_elements(elem.name)) Some(depth + 1) else None
   1.242 +        case (depth, _) => Some(depth + 1)
   1.243        })
   1.244  }