# HG changeset patch # User wenzelm # Date 1396554948 -7200 # Node ID 0546e036d1c084d569e614a82b9ad7e5e88afc05 # Parent bbf4d512f3953d11831de0bdbe10864aa09bc335 more direct warning within persistent Protocol.Status; consider Markup.ERROR (e.g. from Output.error_message without exception) as failure; tuned; diff -r bbf4d512f395 -r 0546e036d1c0 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Thu Apr 03 21:08:00 2014 +0200 +++ b/src/Pure/PIDE/command.scala Thu Apr 03 21:55:48 2014 +0200 @@ -109,7 +109,18 @@ results: Results = Results.empty, markups: Markups = Markups.empty) { - lazy val protocol_status: Protocol.Status = Protocol.Status.make(status.iterator) + lazy val protocol_status: Protocol.Status = + { + val warnings = + if (results.iterator.exists(p => Protocol.is_warning(p._2))) + List(Markup(Markup.WARNING, Nil)) + else Nil + val errors = + if (results.iterator.exists(p => Protocol.is_error(p._2))) + List(Markup(Markup.ERROR, Nil)) + else Nil + Protocol.Status.make((warnings ::: errors ::: status).iterator) + } def markup(index: Markup_Index): Markup_Tree = markups(index) @@ -126,7 +137,7 @@ private def add_markup(status: Boolean, file_name: String, m: Text.Markup): State = { val markups1 = - if (status || Protocol.status_elements(m.info.name)) + if (status || Protocol.liberal_status_elements(m.info.name)) markups.add(Markup_Index(true, file_name), m) else markups copy(markups = markups1.add(Markup_Index(false, file_name), m)) diff -r bbf4d512f395 -r 0546e036d1c0 src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Thu Apr 03 21:08:00 2014 +0200 +++ b/src/Pure/PIDE/protocol.scala Thu Apr 03 21:55:48 2014 +0200 @@ -47,6 +47,7 @@ { var touched = false var accepted = false + var warned = false var failed = false var forks = 0 var runs = 0 @@ -57,11 +58,12 @@ case Markup.JOINED => forks -= 1 case Markup.RUNNING => touched = true; runs += 1 case Markup.FINISHED => runs -= 1 - case Markup.FAILED => failed = true + case Markup.WARNING => warned = true + case Markup.FAILED | Markup.ERROR => failed = true case _ => } } - Status(touched, accepted, failed, forks, runs) + Status(touched, accepted, warned, failed, forks, runs) } val empty = make(Iterator.empty) @@ -77,26 +79,33 @@ sealed case class Status( private val touched: Boolean, private val accepted: Boolean, + private val warned: Boolean, private val failed: Boolean, forks: Int, runs: Int) { def + (that: Status): Status = - Status(touched || that.touched, accepted || that.accepted, failed || that.failed, - forks + that.forks, runs + that.runs) + Status( + touched || that.touched, + accepted || that.accepted, + warned || that.warned, + failed || that.failed, + forks + that.forks, + runs + that.runs) def is_unprocessed: Boolean = accepted && !failed && (!touched || (forks != 0 && runs == 0)) def is_running: Boolean = runs != 0 def is_finished: Boolean = !failed && touched && forks == 0 && runs == 0 + def is_warned: Boolean = is_finished && warned def is_failed: Boolean = failed } - val command_status_elements = + val proper_status_elements = Document.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING, Markup.FINISHED, Markup.FAILED) - val status_elements = - command_status_elements + Markup.WARNING + Markup.ERROR + val liberal_status_elements = + proper_status_elements + Markup.WARNING + Markup.ERROR /* command timing */ @@ -136,10 +145,8 @@ val status = Status.merge(states.iterator.map(_.protocol_status)) if (status.is_running) running += 1 - else if (status.is_finished) { - val warning = states.exists(st => st.results.iterator.exists(p => is_warning(p._2))) - if (warning) warned += 1 else finished += 1 - } + else if (status.is_warned) warned += 1 + else if (status.is_finished) finished += 1 else if (status.is_failed) failed += 1 else unprocessed += 1 } diff -r bbf4d512f395 -r 0546e036d1c0 src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Thu Apr 03 21:08:00 2014 +0200 +++ b/src/Tools/jEdit/src/rendering.scala Thu Apr 03 21:55:48 2014 +0200 @@ -182,7 +182,7 @@ Document.Elements(Markup.SEPARATOR) private val background_elements = - Protocol.command_status_elements + Markup.WRITELN_MESSAGE + + Protocol.proper_status_elements + Markup.WRITELN_MESSAGE + Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY ++ active_elements @@ -292,26 +292,18 @@ if (snapshot.is_outdated) None else { val results = - snapshot.cumulate[(List[Markup], Int)]( - range, (Nil, 0), Protocol.status_elements, _ => + snapshot.cumulate[List[Markup]](range, Nil, Protocol.liberal_status_elements, _ => { - case ((status, pri), Text.Info(_, elem)) => - if (Protocol.command_status_elements(elem.name)) - Some((elem.markup :: status), pri) - else - Some((status, pri max Rendering.message_pri(elem.name))) + case (status, Text.Info(_, elem)) => Some(elem.markup :: status) }, status = true) if (results.isEmpty) None else { - val status = - Protocol.Status.make(results.iterator.flatMap(info => info.info._1.iterator)) - val pri = (0 /: results.iterator.map(info => info.info._2))(_ max _) + val status = Protocol.Status.make(results.iterator.flatMap(_.info)) if (status.is_running) Some(running_color) - else if (pri == Rendering.warning_pri) Some(warning_color) - else if (pri == Rendering.error_pri) Some(error_color) + else if (status.is_warned) Some(warning_color) + else if (status.is_failed) Some(error_color) else if (status.is_unprocessed) Some(unprocessed_color) - else if (status.is_failed) Some(error_color) else None } } @@ -606,7 +598,7 @@ command_states => { case (((status, color), Text.Info(_, XML.Elem(markup, _)))) - if !status.isEmpty && Protocol.command_status_elements(markup.name) => + if !status.isEmpty && Protocol.proper_status_elements(markup.name) => Some((markup :: status, color)) case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) => Some((Nil, Some(bad_color)))