# HG changeset patch # User wenzelm # Date 1607614556 -3600 # Node ID 015a61936c1300b51b3ce30244b84e4b0ae4d740 # Parent 90e28f005be98e1cc2251ed33c541c48befe610f clarified signature: more specific types; diff -r 90e28f005be9 -r 015a61936c13 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Thu Dec 10 15:27:41 2020 +0100 +++ b/src/Pure/PIDE/command.scala Thu Dec 10 16:35:56 2020 +0100 @@ -54,17 +54,17 @@ object Results { - type Entry = (Long, XML.Tree) + type Entry = (Long, XML.Elem) val empty: Results = new Results(SortedMap.empty) def make(args: TraversableOnce[Results.Entry]): Results = (empty /: args)(_ + _) def merge(args: TraversableOnce[Results]): Results = (empty /: args)(_ ++ _) } - final class Results private(private val rep: SortedMap[Long, XML.Tree]) + final class Results private(private val rep: SortedMap[Long, XML.Elem]) { def is_empty: Boolean = rep.isEmpty def defined(serial: Long): Boolean = rep.isDefinedAt(serial) - def get(serial: Long): Option[XML.Tree] = rep.get(serial) + def get(serial: Long): Option[XML.Elem] = rep.get(serial) def iterator: Iterator[Results.Entry] = rep.iterator def + (entry: Results.Entry): Results = @@ -187,15 +187,15 @@ object State { - def get_result(states: List[State], serial: Long): Option[XML.Tree] = + def get_result(states: List[State], serial: Long): Option[XML.Elem] = states.find(st => st.results.defined(serial)).map(st => st.results.get(serial).get) def get_result_proper(states: List[State], props: Properties.T): Option[Results.Entry] = for { serial <- Markup.Serial.unapply(props) - tree @ XML.Elem(_, body) <- get_result(states, serial) - if body.nonEmpty - } yield (serial -> tree) + elem <- get_result(states, serial) + if elem.body.nonEmpty + } yield serial -> elem def merge_results(states: List[State]): Results = Results.merge(states.map(_.results)) diff -r 90e28f005be9 -r 015a61936c13 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Thu Dec 10 15:27:41 2020 +0100 +++ b/src/Pure/PIDE/document.scala Thu Dec 10 16:35:56 2020 +0100 @@ -637,14 +637,14 @@ /* messages */ - lazy val messages: List[(XML.Tree, Position.T)] = + lazy val messages: List[(XML.Elem, Position.T)] = (for { (command, start) <- Document.Node.Commands.starts_pos( node.commands.iterator, Token.Pos.file(node_name.node)) pos = command.span.keyword_pos(start).position(command.span.name) - (_, tree) <- state.command_results(version, command).iterator - } yield (tree, pos)).toList + (_, elem) <- state.command_results(version, command).iterator + } yield (elem, pos)).toList /* exports */ diff -r 90e28f005be9 -r 015a61936c13 src/Pure/PIDE/rendering.scala --- a/src/Pure/PIDE/rendering.scala Thu Dec 10 15:27:41 2020 +0100 +++ b/src/Pure/PIDE/rendering.scala Thu Dec 10 16:35:56 2020 +0100 @@ -11,6 +11,9 @@ import java.io.{File => JFile} import java.nio.file.FileSystems +import scala.collection.immutable.SortedMap + + object Rendering { @@ -94,7 +97,7 @@ legacy_pri -> Color.legacy_message, error_pri -> Color.error_message) - def output_messages(results: Command.Results): List[XML.Tree] = + def output_messages(results: Command.Results): List[XML.Elem] = { val (states, other) = results.iterator.map(_._2).filterNot(Protocol.is_result).toList @@ -537,10 +540,10 @@ } yield Text.Info(r, color) } - def text_messages(range: Text.Range): List[Text.Info[XML.Tree]] = + def text_messages(range: Text.Range): List[Text.Info[XML.Elem]] = { val results = - snapshot.cumulate[Vector[XML.Tree]](range, Vector.empty, Rendering.message_elements, + snapshot.cumulate[Vector[XML.Elem]](range, Vector.empty, Rendering.message_elements, states => { case (res, Text.Info(_, elem)) => @@ -557,17 +560,16 @@ }) var seen_serials = Set.empty[Long] - val seen: XML.Tree => Boolean = - { - case XML.Elem(Markup(_, Markup.Serial(i)), _) => - val b = seen_serials(i); seen_serials += i; b - case _ => false - } + def seen(elem: XML.Elem): Boolean = + elem.markup.properties match { + case Markup.Serial(i) => val b = seen_serials(i); seen_serials += i; b + case _ => false + } for { - Text.Info(range, trees) <- results - tree <- trees - if !seen(tree) - } yield Text.Info(range, tree) + Text.Info(range, elems) <- results + elem <- elems + if !seen(elem) + } yield Text.Info(range, elem) } @@ -578,7 +580,7 @@ private sealed case class Tooltip_Info( range: Text.Range, timing: Timing = Timing.zero, - messages: List[Command.Results.Entry] = Nil, + messages: List[(Long, XML.Tree)] = Nil, rev_infos: List[(Boolean, XML.Tree)] = Nil) { def + (t: Timing): Tooltip_Info = copy(timing = timing + t) @@ -688,7 +690,8 @@ else { val r = Text.Range(results.head.range.start, results.last.range.stop) val all_tips = - Command.Results.make(results.flatMap(_.messages)).iterator.map(_._2).toList ::: + (SortedMap.empty[Long, XML.Tree] /: results.flatMap(_.messages))(_ + _) + .iterator.map(_._2).toList ::: results.flatMap(res => res.infos(true)) ::: results.flatMap(res => res.infos(false)).lastOption.toList if (all_tips.isEmpty) None else Some(Text.Info(r, all_tips)) diff -r 90e28f005be9 -r 015a61936c13 src/Pure/Tools/build_job.scala --- a/src/Pure/Tools/build_job.scala Thu Dec 10 15:27:41 2020 +0100 +++ b/src/Pure/Tools/build_job.scala Thu Dec 10 16:35:56 2020 +0100 @@ -36,9 +36,9 @@ val results = Command.Results.make( for { - tree @ XML.Elem(markup, _) <- read_xml(Export.MESSAGES) + elem @ XML.Elem(markup, _) <- read_xml(Export.MESSAGES) i <- Markup.Serial.unapply(markup.properties) - } yield i -> tree) + } yield i -> elem) val blobs = blobs_files.map(file => diff -r 90e28f005be9 -r 015a61936c13 src/Pure/Tools/dump.scala --- a/src/Pure/Tools/dump.scala Thu Dec 10 15:27:41 2020 +0100 +++ b/src/Pure/Tools/dump.scala Thu Dec 10 16:35:56 2020 +0100 @@ -327,10 +327,10 @@ } else { val msgs = - for ((tree, pos) <- snapshot.messages if Protocol.is_error(tree)) + for ((elem, pos) <- snapshot.messages if Protocol.is_error(elem)) yield { "Error" + Position.here(pos) + ":\n" + - XML.content(Pretty.formatted(List(tree))) + XML.content(Pretty.formatted(List(elem))) } progress.echo("FAILED to process theory " + name) msgs.foreach(progress.echo_error_message)