1.1 --- a/src/Pure/PIDE/document.scala	Fri Feb 21 15:22:06 2014 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Fri Feb 21 15:48:04 2014 +0100
     1.3 @@ -368,24 +368,18 @@
     1.4      val thy_load_commands: List[Command]
     1.5      def eq_content(other: Snapshot): Boolean
     1.6  
     1.7 -    def cumulate_status[A](
     1.8 +    def cumulate[A](
     1.9        range: Text.Range,
    1.10        info: A,
    1.11        elements: String => Boolean,
    1.12 -      result: Command.State => (A, Text.Markup) => Option[A]): List[Text.Info[A]]
    1.13 -    def select_status[A](
    1.14 +      result: Command.State => (A, Text.Markup) => Option[A],
    1.15 +      status: Boolean = false): List[Text.Info[A]]
    1.16 +
    1.17 +    def select[A](
    1.18        range: Text.Range,
    1.19        elements: String => Boolean,
    1.20 -      result: Command.State => Text.Markup => Option[A]): List[Text.Info[A]]
    1.21 -    def cumulate_markup[A](
    1.22 -      range: Text.Range,
    1.23 -      info: A,
    1.24 -      elements: String => Boolean,
    1.25 -      result: Command.State => (A, Text.Markup) => Option[A]): List[Text.Info[A]]
    1.26 -    def select_markup[A](
    1.27 -      range: Text.Range,
    1.28 -      elements: String => Boolean,
    1.29 -      result: Command.State => Text.Markup => Option[A]): List[Text.Info[A]]
    1.30 +      result: Command.State => Text.Markup => Option[A],
    1.31 +      status: Boolean = false): List[Text.Info[A]]
    1.32    }
    1.33  
    1.34    type Assign_Update =
    1.35 @@ -643,12 +637,12 @@
    1.36  
    1.37          /* cumulate markup */
    1.38  
    1.39 -        private def cumulate[A](
    1.40 -          status: Boolean,
    1.41 +        def cumulate[A](
    1.42            range: Text.Range,
    1.43            info: A,
    1.44            elements: String => Boolean,
    1.45 -          result: Command.State => (A, Text.Markup) => Option[A]): List[Text.Info[A]] =
    1.46 +          result: Command.State => (A, Text.Markup) => Option[A],
    1.47 +          status: Boolean = false): List[Text.Info[A]] =
    1.48          {
    1.49            val former_range = revert(range)
    1.50            thy_load_commands match {
    1.51 @@ -680,8 +674,11 @@
    1.52            }
    1.53          }
    1.54  
    1.55 -        private def select[A](status: Boolean, range: Text.Range, elements: String => Boolean,
    1.56 -          result: Command.State => Text.Markup => Option[A]): List[Text.Info[A]] =
    1.57 +        def select[A](
    1.58 +          range: Text.Range,
    1.59 +          elements: String => Boolean,
    1.60 +          result: Command.State => Text.Markup => Option[A],
    1.61 +          status: Boolean = false): List[Text.Info[A]] =
    1.62          {
    1.63            def result1(st: Command.State): (Option[A], Text.Markup) => Option[Option[A]] =
    1.64            {
    1.65 @@ -692,25 +689,9 @@
    1.66                  case some => Some(some)
    1.67                }
    1.68            }
    1.69 -          for (Text.Info(r, Some(x)) <- cumulate_markup(range, None, elements, result1 _))
    1.70 +          for (Text.Info(r, Some(x)) <- cumulate(range, None, elements, result1 _, status))
    1.71              yield Text.Info(r, x)
    1.72          }
    1.73 -
    1.74 -        def cumulate_status[A](range: Text.Range, info: A, elements: String => Boolean,
    1.75 -            result: Command.State => (A, Text.Markup) => Option[A]): List[Text.Info[A]] =
    1.76 -          cumulate(true, range, info, elements, result)
    1.77 -
    1.78 -        def select_status[A](range: Text.Range, elements: String => Boolean,
    1.79 -            result: Command.State => Text.Markup => Option[A]): List[Text.Info[A]] =
    1.80 -          select(true, range, elements, result)
    1.81 -
    1.82 -        def cumulate_markup[A](range: Text.Range, info: A, elements: String => Boolean,
    1.83 -            result: Command.State => (A, Text.Markup) => Option[A]): List[Text.Info[A]] =
    1.84 -          cumulate(false, range, info, elements, result)
    1.85 -
    1.86 -        def select_markup[A](range: Text.Range, elements: String => Boolean,
    1.87 -            result: Command.State => Text.Markup => Option[A]): List[Text.Info[A]] =
    1.88 -          select(false, range, elements, result)
    1.89        }
    1.90      }
    1.91    }

     2.1 --- a/src/Tools/jEdit/src/rendering.scala	Fri Feb 21 15:22:06 2014 +0100
     2.2 +++ b/src/Tools/jEdit/src/rendering.scala	Fri Feb 21 15:48:04 2014 +0100
     2.3 @@ -274,7 +274,7 @@
     2.4    def completion_context(caret: Text.Offset): Option[Completion.Context] =
     2.5      if (caret > 0) {
     2.6        val result =
     2.7 -        snapshot.select_markup(Text.Range(caret - 1, caret + 1), Rendering.completion_elements, _ =>
     2.8 +        snapshot.select(Text.Range(caret - 1, caret + 1), Rendering.completion_elements, _ =>
     2.9            {
    2.10              case Text.Info(_, elem)
    2.11              if elem.name == Markup.ML_STRING || elem.name == Markup.ML_COMMENT =>
    2.12 @@ -301,7 +301,7 @@
    2.13      if (snapshot.is_outdated) None
    2.14      else {
    2.15        val results =
    2.16 -        snapshot.cumulate_status[(Protocol.Status, Int)](
    2.17 +        snapshot.cumulate[(Protocol.Status, Int)](
    2.18            range, (Protocol.Status.init, 0), Protocol.status_elements, _ =>
    2.19            {
    2.20              case ((status, pri), Text.Info(_, elem)) =>
    2.21 @@ -309,7 +309,7 @@
    2.22                  Some((Protocol.command_status(status, elem.markup), pri))
    2.23                else
    2.24                  Some((status, pri max Rendering.message_pri(elem.name)))
    2.25 -          })
    2.26 +          }, status = true)
    2.27        if (results.isEmpty) None
    2.28        else {
    2.29          val (status, pri) =
    2.30 @@ -331,7 +331,7 @@
    2.31  
    2.32    def highlight(range: Text.Range): Option[Text.Info[Color]] =
    2.33    {
    2.34 -    snapshot.select_markup(range, Rendering.highlight_elements, _ =>
    2.35 +    snapshot.select(range, Rendering.highlight_elements, _ =>
    2.36        {
    2.37          case info => Some(Text.Info(snapshot.convert(info.range), highlight_color))
    2.38        }) match { case Text.Info(_, info) :: _ => Some(info) case _ => None }
    2.39 @@ -356,7 +356,7 @@
    2.40  
    2.41    def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
    2.42    {
    2.43 -    snapshot.cumulate_markup[Vector[Text.Info[PIDE.editor.Hyperlink]]](
    2.44 +    snapshot.cumulate[Vector[Text.Info[PIDE.editor.Hyperlink]]](
    2.45        range, Vector.empty, Rendering.hyperlink_elements, _ =>
    2.46          {
    2.47            case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
    2.48 @@ -400,7 +400,7 @@
    2.49    /* active elements */
    2.50  
    2.51    def active(range: Text.Range): Option[Text.Info[XML.Elem]] =
    2.52 -    snapshot.select_markup(range, Rendering.active_elements, command_state =>
    2.53 +    snapshot.select(range, Rendering.active_elements, command_state =>
    2.54        {
    2.55          case Text.Info(info_range, elem) =>
    2.56            if (elem.name == Markup.DIALOG) {
    2.57 @@ -418,7 +418,7 @@
    2.58    def command_results(range: Text.Range): Command.Results =
    2.59    {
    2.60      val results =
    2.61 -      snapshot.select_markup[Command.Results](range, _ => true, command_state =>
    2.62 +      snapshot.select[Command.Results](range, _ => true, command_state =>
    2.63          { case _ => Some(command_state.results) }).map(_.info)
    2.64      (Command.Results.empty /: results)(_ ++ _)
    2.65    }
    2.66 @@ -429,7 +429,7 @@
    2.67    def tooltip_message(range: Text.Range): Option[Text.Info[XML.Body]] =
    2.68    {
    2.69      val results =
    2.70 -      snapshot.cumulate_markup[List[Text.Info[Command.Results.Entry]]](
    2.71 +      snapshot.cumulate[List[Text.Info[Command.Results.Entry]]](
    2.72          range, Nil, Rendering.tooltip_message_elements, _ =>
    2.73          {
    2.74            case (msgs, Text.Info(info_range,
    2.75 @@ -475,7 +475,7 @@
    2.76      }
    2.77  
    2.78      val results =
    2.79 -      snapshot.cumulate_markup[Text.Info[(Timing, Vector[(Boolean, XML.Tree)])]](
    2.80 +      snapshot.cumulate[Text.Info[(Timing, Vector[(Boolean, XML.Tree)])]](
    2.81          range, Text.Info(range, (Timing.zero, Vector.empty)), Rendering.tooltip_elements, _ =>
    2.82          {
    2.83            case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
    2.84 @@ -533,7 +533,7 @@
    2.85    def gutter_message(range: Text.Range): Option[Icon] =
    2.86    {
    2.87      val results =
    2.88 -      snapshot.cumulate_markup[Int](range, 0, Rendering.gutter_elements, _ =>
    2.89 +      snapshot.cumulate[Int](range, 0, Rendering.gutter_elements, _ =>
    2.90          {
    2.91            case (pri, Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _),
    2.92                List(XML.Elem(Markup(Markup.INFORMATION, _), _))))) =>
    2.93 @@ -565,7 +565,7 @@
    2.94    def squiggly_underline(range: Text.Range): List[Text.Info[Color]] =
    2.95    {
    2.96      val results =
    2.97 -      snapshot.cumulate_markup[Int](range, 0, Rendering.squiggly_elements, _ =>
    2.98 +      snapshot.cumulate[Int](range, 0, Rendering.squiggly_elements, _ =>
    2.99          {
   2.100            case (pri, Text.Info(_, elem)) =>
   2.101              if (Protocol.is_information(elem))
   2.102 @@ -592,7 +592,7 @@
   2.103    def line_background(range: Text.Range): Option[(Color, Boolean)] =
   2.104    {
   2.105      val results =
   2.106 -      snapshot.cumulate_markup[Int](range, 0, Rendering.line_background_elements, _ =>
   2.107 +      snapshot.cumulate[Int](range, 0, Rendering.line_background_elements, _ =>
   2.108          {
   2.109            case (pri, Text.Info(_, elem)) =>
   2.110              if (elem.name == Markup.INFORMATION)
   2.111 @@ -604,7 +604,7 @@
   2.112  
   2.113      val is_separator =
   2.114        pri > 0 &&
   2.115 -      snapshot.cumulate_markup[Boolean](range, false, Rendering.separator_elements, _ =>
   2.116 +      snapshot.cumulate[Boolean](range, false, Rendering.separator_elements, _ =>
   2.117          {
   2.118            case _ => Some(true)
   2.119          }).exists(_.info)
   2.120 @@ -624,7 +624,7 @@
   2.121      else
   2.122        for {
   2.123          Text.Info(r, result) <-
   2.124 -          snapshot.cumulate_markup[(Option[Protocol.Status], Option[Color])](
   2.125 +          snapshot.cumulate[(Option[Protocol.Status], Option[Color])](
   2.126              range, (Some(Protocol.Status.init), None), Rendering.background1_elements,
   2.127              command_state =>
   2.128                {
   2.129 @@ -658,13 +658,13 @@
   2.130    }
   2.131  
   2.132    def background2(range: Text.Range): List[Text.Info[Color]] =
   2.133 -    snapshot.select_markup(range, Rendering.background2_elements, _ => _ => Some(light_color))
   2.134 +    snapshot.select(range, Rendering.background2_elements, _ => _ => Some(light_color))
   2.135  
   2.136  
   2.137    /* text foreground */
   2.138  
   2.139    def foreground(range: Text.Range): List[Text.Info[Color]] =
   2.140 -    snapshot.select_markup(range, Rendering.foreground_elements, _ =>
   2.141 +    snapshot.select(range, Rendering.foreground_elements, _ =>
   2.142        {
   2.143          case Text.Info(_, elem) =>
   2.144            if (elem.name == Markup.ANTIQUOTED) Some(antiquoted_color) else Some(quoted_color)
   2.145 @@ -708,7 +708,7 @@
   2.146    {
   2.147      if (color == Token_Markup.hidden_color) List(Text.Info(range, color))
   2.148      else
   2.149 -      snapshot.cumulate_markup(range, color, text_color_elements, _ =>
   2.150 +      snapshot.cumulate(range, color, text_color_elements, _ =>
   2.151          {
   2.152            case (_, Text.Info(_, elem)) => text_colors.get(elem.name)
   2.153          })
   2.154 @@ -718,13 +718,13 @@
   2.155    /* virtual bullets */
   2.156  
   2.157    def bullet(range: Text.Range): List[Text.Info[Color]] =
   2.158 -    snapshot.select_markup(range, Rendering.bullet_elements, _ => _ => Some(bullet_color))
   2.159 +    snapshot.select(range, Rendering.bullet_elements, _ => _ => Some(bullet_color))
   2.160  
   2.161  
   2.162    /* text folds */
   2.163  
   2.164    def fold_depth(range: Text.Range): List[Text.Info[Int]] =
   2.165 -    snapshot.cumulate_markup[Int](range, 0, Rendering.fold_depth_elements, _ =>
   2.166 +    snapshot.cumulate[Int](range, 0, Rendering.fold_depth_elements, _ =>
   2.167        {
   2.168          case (depth, _) => Some(depth + 1)
   2.169        })