--- a/NEWS Fri Dec 11 17:29:42 2020 +0100
+++ b/NEWS Fri Dec 11 17:58:01 2020 +0100
@@ -223,6 +223,12 @@
*** System ***
+* The command-line tool "isabelle log" prints prover messages from the
+build database of the given session, following the the order of theory
+sources, instead of erratic parallel evaluation. Consequently, the
+session log file is restricted to system messages of the overall build
+process, and thus becomes more informative.
+
* Update/rebuild external provers on currently supported OS platforms,
notably CVC4 1.8, E prover 2.5, SPASS 3.8ds, CSDP 6.1.1.
--- a/src/Doc/System/Sessions.thy Fri Dec 11 17:29:42 2020 +0100
+++ b/src/Doc/System/Sessions.thy Fri Dec 11 17:58:01 2020 +0100
@@ -509,6 +509,57 @@
\<close>
+section \<open>Print messages from build database \label{sec:tool-log}\<close>
+
+text \<open>
+ The @{tool_def "log"} tool prints prover messages from the build
+ database of the given session. Its command-line usage is:
+
+ @{verbatim [display]
+\<open>Usage: isabelle log [OPTIONS] SESSION
+
+ Options are:
+ -T NAME restrict to given theories (multiple options possible)
+ -U output Unicode symbols
+ -m MARGIN margin for pretty printing (default: 76.0)
+ -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
+
+ Print messages from the build database of the given session, without any
+ checks against current sources: results from a failed build can be
+ printed as well.\<close>}
+
+ The specified session database is taken as is, independently of the current
+ session structure and theories sources. The order of messages follows the
+ source positions of source files; thus the erratic evaluation of parallel
+ processing rarely matters. There is \<^emph>\<open>no\<close> implicit build process involved,
+ so it is possible to retrieve error messages from a failed session as well.
+
+ \<^medskip> Option \<^verbatim>\<open>-o\<close> allows to change system options, as in @{tool build}
+ (\secref{sec:tool-build}). This may affect the storage space for the build
+ database, notably via @{system_option system_heaps}, or @{system_option
+ build_database_server} and its relatives.
+
+ \<^medskip> Option \<^verbatim>\<open>-T\<close> restricts output to given theories: multiple entries are
+ possible by repeating this option on the command-line. The default is to
+ refer to \<^emph>\<open>all\<close> theories that were used in original session build process.
+
+ \<^medskip> Options \<^verbatim>\<open>-m\<close> and \<^verbatim>\<open>-U\<close> modify pretty printing and output of Isabelle
+ symbols. The default is for an old-fashioned ASCII terminal at 80 characters
+ per line (76 + 4 characters to prefix warnings or errors).
+
+ \<^medskip> Option \<^verbatim>\<open>-v\<close> prints all messages from the session database, including
+ extra information and tracing messages etc.
+\<close>
+
+subsubsection \<open>Examples\<close>
+
+text \<open>
+ Print messages from theory \<^verbatim>\<open>HOL.Nat\<close> of session \<^verbatim>\<open>HOL\<close>, using Unicode
+ rendering of Isabelle symbols and a margin of 100 characters:
+ @{verbatim [display] \<open>isabelle log -T HOL.Nat -U -m 100 HOL\<close>}
+\<close>
+
+
section \<open>Retrieve theory exports \label{sec:tool-export}\<close>
text \<open>
--- a/src/Pure/General/symbol.scala Fri Dec 11 17:29:42 2020 +0100
+++ b/src/Pure/General/symbol.scala Fri Dec 11 17:58:01 2020 +0100
@@ -537,6 +537,9 @@
}
}
+ def output(unicode_symbols: Boolean, text: String): String =
+ if (unicode_symbols) Symbol.decode(text) else Symbol.encode(text)
+
def fonts: Map[Symbol, String] = symbols.fonts
def font_names: List[String] = symbols.font_names
def font_index: Map[String, Int] = symbols.font_index
--- a/src/Pure/PIDE/command.scala Fri Dec 11 17:29:42 2020 +0100
+++ b/src/Pure/PIDE/command.scala Fri Dec 11 17:58:01 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))
--- a/src/Pure/PIDE/document.scala Fri Dec 11 17:29:42 2020 +0100
+++ b/src/Pure/PIDE/document.scala Fri Dec 11 17:58:01 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 */
--- a/src/Pure/PIDE/protocol.scala Fri Dec 11 17:29:42 2020 +0100
+++ b/src/Pure/PIDE/protocol.scala Fri Dec 11 17:58:01 2020 +0100
@@ -116,12 +116,6 @@
/* result messages */
- def is_message(pred: XML.Elem => Boolean, body: XML.Body): Boolean =
- body match {
- case List(elem: XML.Elem) => pred(elem)
- case _ => false
- }
-
def is_result(msg: XML.Tree): Boolean =
msg match {
case XML.Elem(Markup(Markup.RESULT, _), _) => true
@@ -183,18 +177,36 @@
def is_exported(msg: XML.Tree): Boolean =
is_writeln(msg) || is_warning(msg) || is_legacy(msg) || is_error(msg)
- def message_text(body: XML.Body,
+ def message_text(elem: XML.Elem,
+ heading: Boolean = false,
+ pos: Position.T = Position.none,
margin: Double = Pretty.default_margin,
breakgain: Double = Pretty.default_breakgain,
metric: Pretty.Metric = Pretty.Default_Metric): String =
{
- val text =
- Pretty.string_of(Protocol_Message.expose_no_reports(body),
+ val text1 =
+ if (heading) {
+ val h =
+ if (is_warning(elem) || is_legacy(elem)) "Warning"
+ else if (is_error(elem)) "Error"
+ else if (is_information(elem)) "Information"
+ else if (is_tracing(elem)) "Tracing"
+ else if (is_state(elem)) "State"
+ else "Output"
+ "\n" + h + Position.here(pos) + ":\n"
+ }
+ else ""
+
+ val body =
+ Pretty.string_of(Protocol_Message.expose_no_reports(List(elem)),
margin = margin, breakgain = breakgain, metric = metric)
- if (is_message(is_warning, body) || is_message(is_legacy, body)) Output.warning_prefix(text)
- else if (is_message(is_error, body)) Output.error_prefix(text)
- else text
+ val text2 =
+ if (is_warning(elem) || is_legacy(elem)) Output.warning_prefix(body)
+ else if (is_error(elem)) Output.error_prefix(body)
+ else body
+
+ text1 + text2
}
--- a/src/Pure/PIDE/rendering.scala Fri Dec 11 17:29:42 2020 +0100
+++ b/src/Pure/PIDE/rendering.scala Fri Dec 11 17:58:01 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,37 +540,29 @@
} 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,
- states =>
+ snapshot.cumulate[Vector[Command.Results.Entry]](
+ range, Vector.empty, Rendering.message_elements, command_states =>
{
case (res, Text.Info(_, elem)) =>
- elem.markup.properties match {
- case Markup.Serial(i) =>
- states.collectFirst(
- {
- case st if st.results.get(i).isDefined =>
- res :+ st.results.get(i).get
- })
- case _ => None
- }
+ Command.State.get_result_proper(command_states, elem.markup.properties)
+ .map(res :+ _)
case _ => None
})
var seen_serials = Set.empty[Long]
- val seen: XML.Tree => Boolean =
+ def seen(i: Long): Boolean =
{
- case XML.Elem(Markup(_, Markup.Serial(i)), _) =>
- val b = seen_serials(i); seen_serials += i; b
- case _ => false
+ val b = seen_serials(i)
+ seen_serials += i
+ b
}
for {
- Text.Info(range, trees) <- results
- tree <- trees
- if !seen(tree)
- } yield Text.Info(range, tree)
+ Text.Info(range, entries) <- results
+ (i, elem) <- entries if !seen(i)
+ } yield Text.Info(range, elem)
}
@@ -578,7 +573,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 +683,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))
--- a/src/Pure/Thy/presentation.scala Fri Dec 11 17:29:42 2020 +0100
+++ b/src/Pure/Thy/presentation.scala Fri Dec 11 17:58:01 2020 +0100
@@ -60,7 +60,7 @@
def log: String = log_xz.uncompress().text
def log_lines: List[String] = split_lines(log)
- def write(db: SQL.Database, session_name: String) =
+ def write(db: SQL.Database, session_name: String): Unit =
write_document(db, session_name, this)
}
@@ -448,6 +448,9 @@
def tex_name(name: Document.Node.Name): String = name.theory_base_name + ".tex"
def document_tex_name(name: Document.Node.Name): String = "document/" + tex_name(name)
+ class Build_Error(val log_lines: List[String], val message: String)
+ extends Exn.User_Error(message)
+
def build_documents(
session: String,
deps: Sessions.Deps,
@@ -576,14 +579,19 @@
val root_pdf = Path.basic(root).pdf
val result_path = doc_dir + root_pdf
+ val log_lines = result.out_lines ::: result.err_lines
+
if (!result.ok) {
- cat_error(
- Library.trim_line(result.err),
- cat_lines(Latex.latex_errors(doc_dir, root) ::: Bibtex.bibtex_errors(doc_dir, root)),
- "Failed to build document " + quote(doc.name))
+ val message =
+ Exn.cat_message(
+ Library.trim_line(result.err),
+ cat_lines(Latex.latex_errors(doc_dir, root) ::: Bibtex.bibtex_errors(doc_dir, root)),
+ "Failed to build document " + quote(doc.name))
+ throw new Build_Error(log_lines, message)
}
else if (!result_path.is_file) {
- error("Bad document result: expected to find " + root_pdf)
+ val message = "Bad document result: expected to find " + root_pdf
+ throw new Build_Error(log_lines, message)
}
else {
val stop = Time.now()
@@ -591,7 +599,7 @@
progress.echo("Finished " + session + "/" + doc.name +
" (" + timing.message_hms + " elapsed time)")
- val log_xz = Bytes(cat_lines(result.out_lines ::: result.err_lines)).compress()
+ val log_xz = Bytes(cat_lines(log_lines)).compress()
val pdf = Bytes.read(result_path)
Document_Output(doc.name, sources, log_xz, pdf)
}
--- a/src/Pure/Tools/build_job.scala Fri Dec 11 17:29:42 2020 +0100
+++ b/src/Pure/Tools/build_job.scala Fri Dec 11 17:58:01 2020 +0100
@@ -18,46 +18,57 @@
db_context: Sessions.Database_Context,
resources: Resources,
session: String,
- theory: String): Option[Command] =
+ theory: String,
+ unicode_symbols: Boolean = false): Option[Command] =
{
def read(name: String): Export.Entry =
db_context.get_export(List(session), theory, name)
def read_xml(name: String): XML.Body =
- db_context.xml_cache.body(
- YXML.parse_body(Symbol.decode(UTF8.decode_permissive(read(name).uncompressed))))
+ db_context.xml_cache.body(YXML.parse_body(
+ Symbol.output(unicode_symbols, UTF8.decode_permissive(read(name).uncompressed))))
(read(Export.DOCUMENT_ID).text, split_lines(read(Export.FILES).text)) match {
case (Value.Long(id), thy_file :: blobs_files) =>
val thy_path = Path.explode(thy_file)
- val thy_source = Symbol.decode(File.read(thy_path))
val node_name = resources.file_node(thy_path, theory = theory)
+ val results =
+ Command.Results.make(
+ for (elem @ XML.Elem(Markup(_, Markup.Serial(i)), _) <- read_xml(Export.MESSAGES))
+ yield i -> elem)
+
val blobs =
blobs_files.map(file =>
{
val path = Path.explode(file)
+ val name = resources.file_node(path)
val src_path = File.relative_path(thy_path, path).getOrElse(path)
- Command.Blob.read_file(resources.file_node(path), src_path)
+ Command.Blob(name, src_path, None)
})
- val blobs_info = Command.Blobs_Info(blobs.map(Exn.Res(_)))
+ val blobs_xml =
+ for (i <- (1 to blobs.length).toList)
+ yield read_xml(Export.MARKUP + i)
- val results =
- Command.Results.make(
- for {
- tree @ XML.Elem(markup, _) <- read_xml(Export.MESSAGES)
- i <- Markup.Serial.unapply(markup.properties)
- } yield i -> tree)
+ val blobs_info =
+ Command.Blobs_Info(
+ for { (Command.Blob(name, src_path, _), xml) <- blobs zip blobs_xml }
+ yield {
+ val text = XML.content(xml)
+ val chunk = Symbol.Text_Chunk(text)
+ val digest = SHA1.digest(Symbol.encode(text))
+ Exn.Res(Command.Blob(name, src_path, Some((digest, chunk))))
+ })
- val markup_index_blobs =
+ val thy_xml = read_xml(Export.MARKUP)
+ val thy_source = XML.content(thy_xml)
+
+ val markups_index =
Command.Markup_Index.markup :: blobs.map(Command.Markup_Index.blob)
val markups =
Command.Markups.make(
- for ((index, i) <- markup_index_blobs.zipWithIndex)
- yield {
- val xml = read_xml(Export.MARKUP + (if (i == 0) "" else i.toString))
- index -> Markup_Tree.from_XML(xml)
- })
+ for ((index, xml) <- markups_index.zip(thy_xml :: blobs_xml))
+ yield index -> Markup_Tree.from_XML(xml))
val command =
Command.unparsed(thy_source, theory = true, id = id, node_name = node_name,
@@ -74,10 +85,12 @@
options: Options,
session_name: String,
theories: List[String] = Nil,
+ verbose: Boolean = false,
progress: Progress = new Progress,
margin: Double = Pretty.default_margin,
breakgain: Double = Pretty.default_breakgain,
- metric: Pretty.Metric = Pretty.Default_Metric)
+ metric: Pretty.Metric = Symbol.Metric,
+ unicode_symbols: Boolean = false)
{
val store = Sessions.store(options)
@@ -102,23 +115,33 @@
val print_theories =
if (theories.isEmpty) used_theories else used_theories.filter(theories.toSet)
for (thy <- print_theories) {
- val thy_heading = "\nTheory " + quote(thy)
- read_theory(db_context, resources, session_name, thy) match {
- case None => progress.echo(thy_heading + ": MISSING")
+ val thy_heading = "\nTheory " + quote(thy) + ":"
+ read_theory(db_context, resources, session_name, thy, unicode_symbols = unicode_symbols)
+ match {
+ case None => progress.echo(thy_heading + " MISSING")
case Some(command) =>
- progress.echo(thy_heading)
val snapshot = Document.State.init.command_snippet(command)
val rendering = new Rendering(snapshot, options, session)
- for (Text.Info(_, t) <- rendering.text_messages(Text.Range.full)) {
- progress.echo(
- Protocol.message_text(List(t), margin = margin, breakgain = breakgain,
- metric = metric))
+ val messages =
+ rendering.text_messages(Text.Range.full)
+ .filter(message => verbose || Protocol.is_exported(message.info))
+ if (messages.nonEmpty) {
+ val line_document = Line.Document(command.source)
+ progress.echo(thy_heading)
+ for (Text.Info(range, elem) <- messages) {
+ val line = line_document.position(range.start).line1
+ val pos = Position.Line_File(line, command.node_name.node)
+ progress.echo(
+ Protocol.message_text(elem, heading = true, pos = pos,
+ margin = margin, breakgain = breakgain, metric = metric))
+ }
}
}
}
if (errors.nonEmpty) {
- progress.echo("\nErrors:\n" + Output.error_message_text(cat_lines(errors)))
+ val msg = Symbol.output(unicode_symbols, cat_lines(errors))
+ progress.echo("\nBuild errors:\n" + Output.error_message_text(msg))
}
if (rc != 0) progress.echo("\n" + Process_Result.print_return_code(rc))
}
@@ -133,25 +156,31 @@
{
/* arguments */
+ var unicode_symbols = false
var theories: List[String] = Nil
var margin = Pretty.default_margin
var options = Options.init()
+ var verbose = false
val getopts = Getopts("""
Usage: isabelle log [OPTIONS] SESSION
Options are:
- -T NAME restrict to given theories (multiple options)
+ -T NAME restrict to given theories (multiple options possible)
+ -U output Unicode symbols
-m MARGIN margin for pretty printing (default: """ + margin + """)
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
+ -v print all messages, including information, tracing etc.
Print messages from the build database of the given session, without any
checks against current sources: results from a failed build can be
printed as well.
""",
"T:" -> (arg => theories = theories ::: List(arg)),
+ "U" -> (_ => unicode_symbols = true),
"m:" -> (arg => margin = Value.Double.parse(arg)),
- "o:" -> (arg => options = options + arg))
+ "o:" -> (arg => options = options + arg),
+ "v" -> (_ => verbose = true))
val more_args = getopts(args)
val session_name =
@@ -162,7 +191,8 @@
val progress = new Console_Progress()
- print_log(options, session_name, theories = theories, margin = margin, progress = progress)
+ print_log(options, session_name, theories = theories, verbose = verbose, margin = margin,
+ progress = progress, unicode_symbols = unicode_symbols)
})
}
@@ -237,7 +267,6 @@
val stdout = new StringBuilder(1000)
val stderr = new StringBuilder(1000)
- val messages = new mutable.ListBuffer[XML.Elem]
val command_timings = new mutable.ListBuffer[Properties.T]
val theory_timings = new mutable.ListBuffer[Properties.T]
val session_timings = new mutable.ListBuffer[Properties.T]
@@ -367,9 +396,6 @@
else if (msg.is_stderr) {
stderr ++= Symbol.encode(XML.content(message))
}
- else if (Protocol.is_exported(message)) {
- messages += message
- }
else if (msg.is_exit) {
val err =
"Prover terminated" +
@@ -418,8 +444,7 @@
val (document_output, document_errors) =
try {
- if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && info.documents.nonEmpty)
- {
+ if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && info.documents.nonEmpty) {
using(store.open_database_context())(db_context =>
{
val documents =
@@ -433,9 +458,12 @@
(documents.flatMap(_.log_lines), Nil)
})
}
- (Nil, Nil)
+ else (Nil, Nil)
}
- catch { case Exn.Interrupt.ERROR(msg) => (Nil, List(msg)) }
+ catch {
+ case exn: Presentation.Build_Error => (exn.log_lines, List(exn.message))
+ case Exn.Interrupt.ERROR(msg) => (Nil, List(msg))
+ }
val result =
{
@@ -448,8 +476,6 @@
val more_output =
Library.trim_line(stdout.toString) ::
- messages.toList.map(message =>
- Symbol.encode(Protocol.message_text(List(message), metric = Symbol.Metric))) :::
command_timings.toList.map(Protocol.Command_Timing_Marker.apply) :::
used_theory_timings.map(Protocol.Theory_Timing_Marker.apply) :::
session_timings.toList.map(Protocol.Session_Timing_Marker.apply) :::
--- a/src/Pure/Tools/dump.scala Fri Dec 11 17:29:42 2020 +0100
+++ b/src/Pure/Tools/dump.scala Fri Dec 11 17:58:01 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)
--- a/src/Pure/Tools/server_commands.scala Fri Dec 11 17:29:42 2020 +0100
+++ b/src/Pure/Tools/server_commands.scala Fri Dec 11 17:58:01 2020 +0100
@@ -237,8 +237,8 @@
args.commit_cleanup_delay.getOrElse(session.default_commit_cleanup_delay),
id = id, progress = progress)
- def output_text(s: String): String =
- if (args.unicode_symbols) Symbol.decode(s) else Symbol.encode(s)
+ def output_text(text: String): String =
+ Symbol.output(args.unicode_symbols, text)
def output_message(tree: XML.Tree, pos: Position.T): JSON.Object.T =
{
--- a/src/Tools/VSCode/src/vscode_resources.scala Fri Dec 11 17:29:42 2020 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala Fri Dec 11 17:58:01 2020 +0100
@@ -337,8 +337,8 @@
/* output text */
- def output_text(s: String): String =
- if (unicode_symbols) Symbol.decode(s) else Symbol.encode(s)
+ def output_text(text: String): String =
+ Symbol.output(unicode_symbols, text)
def output_xml(xml: XML.Tree): String =
output_text(XML.content(xml))
--- a/src/Tools/jEdit/src/jedit_rendering.scala Fri Dec 11 17:29:42 2020 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala Fri Dec 11 17:58:01 2020 +0100
@@ -347,8 +347,7 @@
val pris =
snapshot.cumulate[Int](range, 0, JEdit_Rendering.gutter_elements, _ =>
{
- case (pri, Text.Info(_, msg @ XML.Elem(Markup(_, Markup.Serial(serial)), _))) =>
- Some(pri max gutter_message_pri(msg))
+ case (pri, Text.Info(_, elem)) => Some(pri max gutter_message_pri(elem))
case _ => None
}).map(_.info)