tuned signature -- expose less intermediate information;
authorwenzelm
Wed Mar 26 21:01:09 2014 +0100 (2014-03-26)
changeset 56298cf7710540f39
parent 56297 3925634718fb
child 56299 8201790fdeb9
tuned signature -- expose less intermediate information;
src/Pure/PIDE/document.scala
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Wed Mar 26 20:32:15 2014 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Wed Mar 26 21:01:09 2014 +0100
     1.3 @@ -429,13 +429,13 @@
     1.4        range: Text.Range,
     1.5        info: A,
     1.6        elements: Elements,
     1.7 -      result: Command.State => (A, Text.Markup) => Option[A],
     1.8 +      result: Command.Results => (A, Text.Markup) => Option[A],
     1.9        status: Boolean = false): List[Text.Info[A]]
    1.10  
    1.11      def select[A](
    1.12        range: Text.Range,
    1.13        elements: Elements,
    1.14 -      result: Command.State => Text.Markup => Option[A],
    1.15 +      result: Command.Results => Text.Markup => Option[A],
    1.16        status: Boolean = false): List[Text.Info[A]]
    1.17    }
    1.18  
    1.19 @@ -708,7 +708,7 @@
    1.20            range: Text.Range,
    1.21            info: A,
    1.22            elements: Elements,
    1.23 -          result: Command.State => (A, Text.Markup) => Option[A],
    1.24 +          result: Command.Results => (A, Text.Markup) => Option[A],
    1.25            status: Boolean = false): List[Text.Info[A]] =
    1.26          {
    1.27            val former_range = revert(range)
    1.28 @@ -719,7 +719,7 @@
    1.29                (for {
    1.30                  chunk <- thy_load_command.chunks.get(file_name).iterator
    1.31                  st = state.command_state(version, thy_load_command)
    1.32 -                res = result(st)
    1.33 +                res = result(st.results)
    1.34                  Text.Info(r0, a) <- st.markup(markup_index).cumulate[A](
    1.35                    former_range.restrict(chunk.range), info, elements,
    1.36                    { case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0), b)) }
    1.37 @@ -731,7 +731,7 @@
    1.38                (for {
    1.39                  (command, command_start) <- node.command_range(former_range)
    1.40                  st = state.command_state(version, command)
    1.41 -                res = result(st)
    1.42 +                res = result(st.results)
    1.43                  Text.Info(r0, a) <- st.markup(markup_index).cumulate[A](
    1.44                    (former_range - command_start).restrict(command.range), info, elements,
    1.45                    {
    1.46 @@ -744,12 +744,12 @@
    1.47          def select[A](
    1.48            range: Text.Range,
    1.49            elements: Elements,
    1.50 -          result: Command.State => Text.Markup => Option[A],
    1.51 +          result: Command.Results => Text.Markup => Option[A],
    1.52            status: Boolean = false): List[Text.Info[A]] =
    1.53          {
    1.54 -          def result1(st: Command.State): (Option[A], Text.Markup) => Option[Option[A]] =
    1.55 +          def result1(results: Command.Results): (Option[A], Text.Markup) => Option[Option[A]] =
    1.56            {
    1.57 -            val res = result(st)
    1.58 +            val res = result(results)
    1.59              (_: Option[A], x: Text.Markup) =>
    1.60                res(x) match {
    1.61                  case None => None
     2.1 --- a/src/Tools/jEdit/src/rendering.scala	Wed Mar 26 20:32:15 2014 +0100
     2.2 +++ b/src/Tools/jEdit/src/rendering.scala	Wed Mar 26 21:01:09 2014 +0100
     2.3 @@ -380,13 +380,13 @@
     2.4    /* active elements */
     2.5  
     2.6    def active(range: Text.Range): Option[Text.Info[XML.Elem]] =
     2.7 -    snapshot.select(range, Rendering.active_elements, command_state =>
     2.8 +    snapshot.select(range, Rendering.active_elements, command_results =>
     2.9        {
    2.10          case Text.Info(info_range, elem) =>
    2.11            if (elem.name == Markup.DIALOG) {
    2.12              elem match {
    2.13                case Protocol.Dialog(_, serial, _)
    2.14 -              if !command_state.results.defined(serial) =>
    2.15 +              if !command_results.defined(serial) =>
    2.16                  Some(Text.Info(snapshot.convert(info_range), elem))
    2.17                case _ => None
    2.18              }
    2.19 @@ -397,8 +397,8 @@
    2.20    def command_results(range: Text.Range): Command.Results =
    2.21    {
    2.22      val results =
    2.23 -      snapshot.select[Command.Results](range, Document.Elements.full, command_state =>
    2.24 -        { case _ => Some(command_state.results) }).map(_.info)
    2.25 +      snapshot.select[Command.Results](range, Document.Elements.full, command_results =>
    2.26 +        { case _ => Some(command_results) }).map(_.info)
    2.27      (Command.Results.empty /: results)(_ ++ _)
    2.28    }
    2.29  
    2.30 @@ -606,7 +606,7 @@
    2.31          Text.Info(r, result) <-
    2.32            snapshot.cumulate[(Option[Protocol.Status], Option[Color])](
    2.33              range, (Some(Protocol.Status.init), None), Rendering.background_elements,
    2.34 -            command_state =>
    2.35 +            command_results =>
    2.36                {
    2.37                  case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
    2.38                  if (Protocol.command_status_elements(markup.name)) =>
    2.39 @@ -616,7 +616,7 @@
    2.40                  case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
    2.41                    Some((None, Some(intensify_color)))
    2.42                  case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
    2.43 -                  command_state.results.get(serial) match {
    2.44 +                  command_results.get(serial) match {
    2.45                      case Some(Protocol.Dialog_Result(res)) if res == result =>
    2.46                        Some((None, Some(active_result_color)))
    2.47                      case _ =>