# HG changeset patch # User wenzelm # Date 1395864069 -3600 # Node ID cf7710540f39afeae386ec5acaf32020669df3a4 # Parent 3925634718fb335284091dec75f9fb13302a5f58 tuned signature -- expose less intermediate information; diff -r 3925634718fb -r cf7710540f39 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Wed Mar 26 20:32:15 2014 +0100 +++ b/src/Pure/PIDE/document.scala Wed Mar 26 21:01:09 2014 +0100 @@ -429,13 +429,13 @@ range: Text.Range, info: A, elements: Elements, - result: Command.State => (A, Text.Markup) => Option[A], + result: Command.Results => (A, Text.Markup) => Option[A], status: Boolean = false): List[Text.Info[A]] def select[A]( range: Text.Range, elements: Elements, - result: Command.State => Text.Markup => Option[A], + result: Command.Results => Text.Markup => Option[A], status: Boolean = false): List[Text.Info[A]] } @@ -708,7 +708,7 @@ range: Text.Range, info: A, elements: Elements, - result: Command.State => (A, Text.Markup) => Option[A], + result: Command.Results => (A, Text.Markup) => Option[A], status: Boolean = false): List[Text.Info[A]] = { val former_range = revert(range) @@ -719,7 +719,7 @@ (for { chunk <- thy_load_command.chunks.get(file_name).iterator st = state.command_state(version, thy_load_command) - res = result(st) + res = result(st.results) Text.Info(r0, a) <- st.markup(markup_index).cumulate[A]( former_range.restrict(chunk.range), info, elements, { case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0), b)) } @@ -731,7 +731,7 @@ (for { (command, command_start) <- node.command_range(former_range) st = state.command_state(version, command) - res = result(st) + res = result(st.results) Text.Info(r0, a) <- st.markup(markup_index).cumulate[A]( (former_range - command_start).restrict(command.range), info, elements, { @@ -744,12 +744,12 @@ def select[A]( range: Text.Range, elements: Elements, - result: Command.State => Text.Markup => Option[A], + result: Command.Results => Text.Markup => Option[A], status: Boolean = false): List[Text.Info[A]] = { - def result1(st: Command.State): (Option[A], Text.Markup) => Option[Option[A]] = + def result1(results: Command.Results): (Option[A], Text.Markup) => Option[Option[A]] = { - val res = result(st) + val res = result(results) (_: Option[A], x: Text.Markup) => res(x) match { case None => None diff -r 3925634718fb -r cf7710540f39 src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Wed Mar 26 20:32:15 2014 +0100 +++ b/src/Tools/jEdit/src/rendering.scala Wed Mar 26 21:01:09 2014 +0100 @@ -380,13 +380,13 @@ /* active elements */ def active(range: Text.Range): Option[Text.Info[XML.Elem]] = - snapshot.select(range, Rendering.active_elements, command_state => + snapshot.select(range, Rendering.active_elements, command_results => { case Text.Info(info_range, elem) => if (elem.name == Markup.DIALOG) { elem match { case Protocol.Dialog(_, serial, _) - if !command_state.results.defined(serial) => + if !command_results.defined(serial) => Some(Text.Info(snapshot.convert(info_range), elem)) case _ => None } @@ -397,8 +397,8 @@ def command_results(range: Text.Range): Command.Results = { val results = - snapshot.select[Command.Results](range, Document.Elements.full, command_state => - { case _ => Some(command_state.results) }).map(_.info) + snapshot.select[Command.Results](range, Document.Elements.full, command_results => + { case _ => Some(command_results) }).map(_.info) (Command.Results.empty /: results)(_ ++ _) } @@ -606,7 +606,7 @@ Text.Info(r, result) <- snapshot.cumulate[(Option[Protocol.Status], Option[Color])]( range, (Some(Protocol.Status.init), None), Rendering.background_elements, - command_state => + command_results => { case (((Some(status), color), Text.Info(_, XML.Elem(markup, _)))) if (Protocol.command_status_elements(markup.name)) => @@ -616,7 +616,7 @@ case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) => Some((None, Some(intensify_color))) case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) => - command_state.results.get(serial) match { + command_results.get(serial) match { case Some(Protocol.Dialog_Result(res)) if res == result => Some((None, Some(active_result_color))) case _ =>