# HG changeset patch # User wenzelm # Date 1392994084 -3600 # Node ID fa42cf3fe79b2c823298ee4b6eba6c254dfa33d3 # Parent 349afd0fa0c4b942203d91cdeefb10a62fac2365 tuned signature -- avoid redundancy and confusion of flags; diff -r 349afd0fa0c4 -r fa42cf3fe79b src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Fri Feb 21 15:22:06 2014 +0100 +++ b/src/Pure/PIDE/document.scala Fri Feb 21 15:48:04 2014 +0100 @@ -368,24 +368,18 @@ val thy_load_commands: List[Command] def eq_content(other: Snapshot): Boolean - def cumulate_status[A]( + def cumulate[A]( range: Text.Range, info: A, elements: String => Boolean, - result: Command.State => (A, Text.Markup) => Option[A]): List[Text.Info[A]] - def select_status[A]( + result: Command.State => (A, Text.Markup) => Option[A], + status: Boolean = false): List[Text.Info[A]] + + def select[A]( range: Text.Range, elements: String => Boolean, - result: Command.State => Text.Markup => Option[A]): List[Text.Info[A]] - def cumulate_markup[A]( - range: Text.Range, - info: A, - elements: String => Boolean, - result: Command.State => (A, Text.Markup) => Option[A]): List[Text.Info[A]] - def select_markup[A]( - range: Text.Range, - elements: String => Boolean, - result: Command.State => Text.Markup => Option[A]): List[Text.Info[A]] + result: Command.State => Text.Markup => Option[A], + status: Boolean = false): List[Text.Info[A]] } type Assign_Update = @@ -643,12 +637,12 @@ /* cumulate markup */ - private def cumulate[A]( - status: Boolean, + def cumulate[A]( range: Text.Range, info: A, elements: String => Boolean, - result: Command.State => (A, Text.Markup) => Option[A]): List[Text.Info[A]] = + result: Command.State => (A, Text.Markup) => Option[A], + status: Boolean = false): List[Text.Info[A]] = { val former_range = revert(range) thy_load_commands match { @@ -680,8 +674,11 @@ } } - private def select[A](status: Boolean, range: Text.Range, elements: String => Boolean, - result: Command.State => Text.Markup => Option[A]): List[Text.Info[A]] = + def select[A]( + range: Text.Range, + elements: String => Boolean, + result: Command.State => Text.Markup => Option[A], + status: Boolean = false): List[Text.Info[A]] = { def result1(st: Command.State): (Option[A], Text.Markup) => Option[Option[A]] = { @@ -692,25 +689,9 @@ case some => Some(some) } } - for (Text.Info(r, Some(x)) <- cumulate_markup(range, None, elements, result1 _)) + for (Text.Info(r, Some(x)) <- cumulate(range, None, elements, result1 _, status)) yield Text.Info(r, x) } - - def cumulate_status[A](range: Text.Range, info: A, elements: String => Boolean, - result: Command.State => (A, Text.Markup) => Option[A]): List[Text.Info[A]] = - cumulate(true, range, info, elements, result) - - def select_status[A](range: Text.Range, elements: String => Boolean, - result: Command.State => Text.Markup => Option[A]): List[Text.Info[A]] = - select(true, range, elements, result) - - def cumulate_markup[A](range: Text.Range, info: A, elements: String => Boolean, - result: Command.State => (A, Text.Markup) => Option[A]): List[Text.Info[A]] = - cumulate(false, range, info, elements, result) - - def select_markup[A](range: Text.Range, elements: String => Boolean, - result: Command.State => Text.Markup => Option[A]): List[Text.Info[A]] = - select(false, range, elements, result) } } } diff -r 349afd0fa0c4 -r fa42cf3fe79b src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Fri Feb 21 15:22:06 2014 +0100 +++ b/src/Tools/jEdit/src/rendering.scala Fri Feb 21 15:48:04 2014 +0100 @@ -274,7 +274,7 @@ def completion_context(caret: Text.Offset): Option[Completion.Context] = if (caret > 0) { val result = - snapshot.select_markup(Text.Range(caret - 1, caret + 1), Rendering.completion_elements, _ => + snapshot.select(Text.Range(caret - 1, caret + 1), Rendering.completion_elements, _ => { case Text.Info(_, elem) if elem.name == Markup.ML_STRING || elem.name == Markup.ML_COMMENT => @@ -301,7 +301,7 @@ if (snapshot.is_outdated) None else { val results = - snapshot.cumulate_status[(Protocol.Status, Int)]( + snapshot.cumulate[(Protocol.Status, Int)]( range, (Protocol.Status.init, 0), Protocol.status_elements, _ => { case ((status, pri), Text.Info(_, elem)) => @@ -309,7 +309,7 @@ Some((Protocol.command_status(status, elem.markup), pri)) else Some((status, pri max Rendering.message_pri(elem.name))) - }) + }, status = true) if (results.isEmpty) None else { val (status, pri) = @@ -331,7 +331,7 @@ def highlight(range: Text.Range): Option[Text.Info[Color]] = { - snapshot.select_markup(range, Rendering.highlight_elements, _ => + snapshot.select(range, Rendering.highlight_elements, _ => { case info => Some(Text.Info(snapshot.convert(info.range), highlight_color)) }) match { case Text.Info(_, info) :: _ => Some(info) case _ => None } @@ -356,7 +356,7 @@ def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] = { - snapshot.cumulate_markup[Vector[Text.Info[PIDE.editor.Hyperlink]]]( + snapshot.cumulate[Vector[Text.Info[PIDE.editor.Hyperlink]]]( range, Vector.empty, Rendering.hyperlink_elements, _ => { case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _))) @@ -400,7 +400,7 @@ /* active elements */ def active(range: Text.Range): Option[Text.Info[XML.Elem]] = - snapshot.select_markup(range, Rendering.active_elements, command_state => + snapshot.select(range, Rendering.active_elements, command_state => { case Text.Info(info_range, elem) => if (elem.name == Markup.DIALOG) { @@ -418,7 +418,7 @@ def command_results(range: Text.Range): Command.Results = { val results = - snapshot.select_markup[Command.Results](range, _ => true, command_state => + snapshot.select[Command.Results](range, _ => true, command_state => { case _ => Some(command_state.results) }).map(_.info) (Command.Results.empty /: results)(_ ++ _) } @@ -429,7 +429,7 @@ def tooltip_message(range: Text.Range): Option[Text.Info[XML.Body]] = { val results = - snapshot.cumulate_markup[List[Text.Info[Command.Results.Entry]]]( + snapshot.cumulate[List[Text.Info[Command.Results.Entry]]]( range, Nil, Rendering.tooltip_message_elements, _ => { case (msgs, Text.Info(info_range, @@ -475,7 +475,7 @@ } val results = - snapshot.cumulate_markup[Text.Info[(Timing, Vector[(Boolean, XML.Tree)])]]( + snapshot.cumulate[Text.Info[(Timing, Vector[(Boolean, XML.Tree)])]]( range, Text.Info(range, (Timing.zero, Vector.empty)), Rendering.tooltip_elements, _ => { case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) => @@ -533,7 +533,7 @@ def gutter_message(range: Text.Range): Option[Icon] = { val results = - snapshot.cumulate_markup[Int](range, 0, Rendering.gutter_elements, _ => + snapshot.cumulate[Int](range, 0, Rendering.gutter_elements, _ => { case (pri, Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), List(XML.Elem(Markup(Markup.INFORMATION, _), _))))) => @@ -565,7 +565,7 @@ def squiggly_underline(range: Text.Range): List[Text.Info[Color]] = { val results = - snapshot.cumulate_markup[Int](range, 0, Rendering.squiggly_elements, _ => + snapshot.cumulate[Int](range, 0, Rendering.squiggly_elements, _ => { case (pri, Text.Info(_, elem)) => if (Protocol.is_information(elem)) @@ -592,7 +592,7 @@ def line_background(range: Text.Range): Option[(Color, Boolean)] = { val results = - snapshot.cumulate_markup[Int](range, 0, Rendering.line_background_elements, _ => + snapshot.cumulate[Int](range, 0, Rendering.line_background_elements, _ => { case (pri, Text.Info(_, elem)) => if (elem.name == Markup.INFORMATION) @@ -604,7 +604,7 @@ val is_separator = pri > 0 && - snapshot.cumulate_markup[Boolean](range, false, Rendering.separator_elements, _ => + snapshot.cumulate[Boolean](range, false, Rendering.separator_elements, _ => { case _ => Some(true) }).exists(_.info) @@ -624,7 +624,7 @@ else for { Text.Info(r, result) <- - snapshot.cumulate_markup[(Option[Protocol.Status], Option[Color])]( + snapshot.cumulate[(Option[Protocol.Status], Option[Color])]( range, (Some(Protocol.Status.init), None), Rendering.background1_elements, command_state => { @@ -658,13 +658,13 @@ } def background2(range: Text.Range): List[Text.Info[Color]] = - snapshot.select_markup(range, Rendering.background2_elements, _ => _ => Some(light_color)) + snapshot.select(range, Rendering.background2_elements, _ => _ => Some(light_color)) /* text foreground */ def foreground(range: Text.Range): List[Text.Info[Color]] = - snapshot.select_markup(range, Rendering.foreground_elements, _ => + snapshot.select(range, Rendering.foreground_elements, _ => { case Text.Info(_, elem) => if (elem.name == Markup.ANTIQUOTED) Some(antiquoted_color) else Some(quoted_color) @@ -708,7 +708,7 @@ { if (color == Token_Markup.hidden_color) List(Text.Info(range, color)) else - snapshot.cumulate_markup(range, color, text_color_elements, _ => + snapshot.cumulate(range, color, text_color_elements, _ => { case (_, Text.Info(_, elem)) => text_colors.get(elem.name) }) @@ -718,13 +718,13 @@ /* virtual bullets */ def bullet(range: Text.Range): List[Text.Info[Color]] = - snapshot.select_markup(range, Rendering.bullet_elements, _ => _ => Some(bullet_color)) + snapshot.select(range, Rendering.bullet_elements, _ => _ => Some(bullet_color)) /* text folds */ def fold_depth(range: Text.Range): List[Text.Info[Int]] = - snapshot.cumulate_markup[Int](range, 0, Rendering.fold_depth_elements, _ => + snapshot.cumulate[Int](range, 0, Rendering.fold_depth_elements, _ => { case (depth, _) => Some(depth + 1) })