more direct warning within persistent Protocol.Status;
authorwenzelm
Thu Apr 03 21:55:48 2014 +0200 (2014-04-03)
changeset 563950546e036d1c0
parent 56394 bbf4d512f395
child 56396 91a8561a8e35
more direct warning within persistent Protocol.Status;
consider Markup.ERROR (e.g. from Output.error_message without exception) as failure;
tuned;
src/Pure/PIDE/command.scala
src/Pure/PIDE/protocol.scala
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Thu Apr 03 21:08:00 2014 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Thu Apr 03 21:55:48 2014 +0200
     1.3 @@ -109,7 +109,18 @@
     1.4      results: Results = Results.empty,
     1.5      markups: Markups = Markups.empty)
     1.6    {
     1.7 -    lazy val protocol_status: Protocol.Status = Protocol.Status.make(status.iterator)
     1.8 +    lazy val protocol_status: Protocol.Status =
     1.9 +    {
    1.10 +      val warnings =
    1.11 +        if (results.iterator.exists(p => Protocol.is_warning(p._2)))
    1.12 +          List(Markup(Markup.WARNING, Nil))
    1.13 +        else Nil
    1.14 +      val errors =
    1.15 +        if (results.iterator.exists(p => Protocol.is_error(p._2)))
    1.16 +          List(Markup(Markup.ERROR, Nil))
    1.17 +        else Nil
    1.18 +      Protocol.Status.make((warnings ::: errors ::: status).iterator)
    1.19 +    }
    1.20  
    1.21      def markup(index: Markup_Index): Markup_Tree = markups(index)
    1.22  
    1.23 @@ -126,7 +137,7 @@
    1.24      private def add_markup(status: Boolean, file_name: String, m: Text.Markup): State =
    1.25      {
    1.26        val markups1 =
    1.27 -        if (status || Protocol.status_elements(m.info.name))
    1.28 +        if (status || Protocol.liberal_status_elements(m.info.name))
    1.29            markups.add(Markup_Index(true, file_name), m)
    1.30          else markups
    1.31        copy(markups = markups1.add(Markup_Index(false, file_name), m))
     2.1 --- a/src/Pure/PIDE/protocol.scala	Thu Apr 03 21:08:00 2014 +0200
     2.2 +++ b/src/Pure/PIDE/protocol.scala	Thu Apr 03 21:55:48 2014 +0200
     2.3 @@ -47,6 +47,7 @@
     2.4      {
     2.5        var touched = false
     2.6        var accepted = false
     2.7 +      var warned = false
     2.8        var failed = false
     2.9        var forks = 0
    2.10        var runs = 0
    2.11 @@ -57,11 +58,12 @@
    2.12            case Markup.JOINED => forks -= 1
    2.13            case Markup.RUNNING => touched = true; runs += 1
    2.14            case Markup.FINISHED => runs -= 1
    2.15 -          case Markup.FAILED => failed = true
    2.16 +          case Markup.WARNING => warned = true
    2.17 +          case Markup.FAILED | Markup.ERROR => failed = true
    2.18            case _ =>
    2.19          }
    2.20        }
    2.21 -      Status(touched, accepted, failed, forks, runs)
    2.22 +      Status(touched, accepted, warned, failed, forks, runs)
    2.23      }
    2.24  
    2.25      val empty = make(Iterator.empty)
    2.26 @@ -77,26 +79,33 @@
    2.27    sealed case class Status(
    2.28      private val touched: Boolean,
    2.29      private val accepted: Boolean,
    2.30 +    private val warned: Boolean,
    2.31      private val failed: Boolean,
    2.32      forks: Int,
    2.33      runs: Int)
    2.34    {
    2.35      def + (that: Status): Status =
    2.36 -      Status(touched || that.touched, accepted || that.accepted, failed || that.failed,
    2.37 -        forks + that.forks, runs + that.runs)
    2.38 +      Status(
    2.39 +        touched || that.touched,
    2.40 +        accepted || that.accepted,
    2.41 +        warned || that.warned,
    2.42 +        failed || that.failed,
    2.43 +        forks + that.forks,
    2.44 +        runs + that.runs)
    2.45  
    2.46      def is_unprocessed: Boolean = accepted && !failed && (!touched || (forks != 0 && runs == 0))
    2.47      def is_running: Boolean = runs != 0
    2.48      def is_finished: Boolean = !failed && touched && forks == 0 && runs == 0
    2.49 +    def is_warned: Boolean = is_finished && warned
    2.50      def is_failed: Boolean = failed
    2.51    }
    2.52  
    2.53 -  val command_status_elements =
    2.54 +  val proper_status_elements =
    2.55      Document.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
    2.56        Markup.FINISHED, Markup.FAILED)
    2.57  
    2.58 -  val status_elements =
    2.59 -    command_status_elements + Markup.WARNING + Markup.ERROR
    2.60 +  val liberal_status_elements =
    2.61 +    proper_status_elements + Markup.WARNING + Markup.ERROR
    2.62  
    2.63  
    2.64    /* command timing */
    2.65 @@ -136,10 +145,8 @@
    2.66        val status = Status.merge(states.iterator.map(_.protocol_status))
    2.67  
    2.68        if (status.is_running) running += 1
    2.69 -      else if (status.is_finished) {
    2.70 -        val warning = states.exists(st => st.results.iterator.exists(p => is_warning(p._2)))
    2.71 -        if (warning) warned += 1 else finished += 1
    2.72 -      }
    2.73 +      else if (status.is_warned) warned += 1
    2.74 +      else if (status.is_finished) finished += 1
    2.75        else if (status.is_failed) failed += 1
    2.76        else unprocessed += 1
    2.77      }
     3.1 --- a/src/Tools/jEdit/src/rendering.scala	Thu Apr 03 21:08:00 2014 +0200
     3.2 +++ b/src/Tools/jEdit/src/rendering.scala	Thu Apr 03 21:55:48 2014 +0200
     3.3 @@ -182,7 +182,7 @@
     3.4      Document.Elements(Markup.SEPARATOR)
     3.5  
     3.6    private val background_elements =
     3.7 -    Protocol.command_status_elements + Markup.WRITELN_MESSAGE +
     3.8 +    Protocol.proper_status_elements + Markup.WRITELN_MESSAGE +
     3.9        Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE +
    3.10        Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY ++
    3.11        active_elements
    3.12 @@ -292,26 +292,18 @@
    3.13      if (snapshot.is_outdated) None
    3.14      else {
    3.15        val results =
    3.16 -        snapshot.cumulate[(List[Markup], Int)](
    3.17 -          range, (Nil, 0), Protocol.status_elements, _ =>
    3.18 +        snapshot.cumulate[List[Markup]](range, Nil, Protocol.liberal_status_elements, _ =>
    3.19            {
    3.20 -            case ((status, pri), Text.Info(_, elem)) =>
    3.21 -              if (Protocol.command_status_elements(elem.name))
    3.22 -                Some((elem.markup :: status), pri)
    3.23 -              else
    3.24 -                Some((status, pri max Rendering.message_pri(elem.name)))
    3.25 +            case (status, Text.Info(_, elem)) => Some(elem.markup :: status)
    3.26            }, status = true)
    3.27        if (results.isEmpty) None
    3.28        else {
    3.29 -        val status =
    3.30 -          Protocol.Status.make(results.iterator.flatMap(info => info.info._1.iterator))
    3.31 -        val pri = (0 /: results.iterator.map(info => info.info._2))(_ max _)
    3.32 +        val status = Protocol.Status.make(results.iterator.flatMap(_.info))
    3.33  
    3.34          if (status.is_running) Some(running_color)
    3.35 -        else if (pri == Rendering.warning_pri) Some(warning_color)
    3.36 -        else if (pri == Rendering.error_pri) Some(error_color)
    3.37 +        else if (status.is_warned) Some(warning_color)
    3.38 +        else if (status.is_failed) Some(error_color)
    3.39          else if (status.is_unprocessed) Some(unprocessed_color)
    3.40 -        else if (status.is_failed) Some(error_color)
    3.41          else None
    3.42        }
    3.43      }
    3.44 @@ -606,7 +598,7 @@
    3.45              command_states =>
    3.46                {
    3.47                  case (((status, color), Text.Info(_, XML.Elem(markup, _))))
    3.48 -                if !status.isEmpty && Protocol.command_status_elements(markup.name) =>
    3.49 +                if !status.isEmpty && Protocol.proper_status_elements(markup.name) =>
    3.50                    Some((markup :: status, color))
    3.51                  case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
    3.52                    Some((Nil, Some(bad_color)))