merged
authornipkow
Fri, 11 Dec 2020 17:58:01 +0100
changeset 72884 50f18a822ee9
parent 72882 1dc2ad97e062 (diff)
parent 72883 4e6dc2868d5f (current diff)
child 72885 1b0f81e556a2
merged
--- 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)