diff -r 080422b3d914 -r 570f65953173 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Mon Mar 06 21:12:47 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Tue Mar 07 10:16:24 2023 +0100
@@ -8,7 +8,6 @@
 
 
 import scala.collection.mutable
-import scala.util.matching.Regex
 
 
 trait Build_Job {
@@ -602,156 +601,4 @@
       Document.State.init.snippet(command, doc_blobs)
     }
   }
-
-
-  /* print messages */
-
-  def print_log(
-    options: Options,
-    sessions: List[String],
-    theories: List[String] = Nil,
-    message_head: List[Regex] = Nil,
-    message_body: List[Regex] = Nil,
-    progress: Progress = new Progress,
-    margin: Double = Pretty.default_margin,
-    breakgain: Double = Pretty.default_breakgain,
-    metric: Pretty.Metric = Symbol.Metric,
-    unicode_symbols: Boolean = false
-  ): Unit = {
-    val store = Sessions.store(options)
-    val session = new Session(options, Resources.bootstrap)
-
-    def check(filter: List[Regex], make_string: => String): Boolean =
-      filter.isEmpty || {
-        val s = Output.clean_yxml(make_string)
-        filter.forall(r => r.findFirstIn(Output.clean_yxml(s)).nonEmpty)
-      }
-
-    def print(session_name: String): Unit = {
-      using(Export.open_session_context0(store, session_name)) { session_context =>
-        val result =
-          for {
-            db <- session_context.session_db()
-            theories = store.read_theories(db, session_name)
-            errors = store.read_errors(db, session_name)
-            info <- store.read_build(db, session_name)
-          } yield (theories, errors, info.return_code)
-        result match {
-          case None => store.error_database(session_name)
-          case Some((used_theories, errors, rc)) =>
-            theories.filterNot(used_theories.toSet) match {
-              case Nil =>
-              case bad => error("Unknown theories " + commas_quote(bad))
-            }
-            val print_theories =
-              if (theories.isEmpty) used_theories else used_theories.filter(theories.toSet)
-
-            for (thy <- print_theories) {
-              val thy_heading = "\nTheory " + quote(thy) + " (in " + session_name + ")" + ":"
-
-              read_theory(session_context.theory(thy), unicode_symbols = unicode_symbols) match {
-                case None => progress.echo(thy_heading + " MISSING")
-                case Some(snapshot) =>
-                  val rendering = new Rendering(snapshot, options, session)
-                  val messages =
-                    rendering.text_messages(Text.Range.full)
-                      .filter(message => progress.verbose || Protocol.is_exported(message.info))
-                  if (messages.nonEmpty) {
-                    val line_document = Line.Document(snapshot.node.source)
-                    val buffer = new mutable.ListBuffer[String]
-                    for (Text.Info(range, elem) <- messages) {
-                      val line = line_document.position(range.start).line1
-                      val pos = Position.Line_File(line, snapshot.node_name.node)
-                      def message_text: String =
-                        Protocol.message_text(elem, heading = true, pos = pos,
-                          margin = margin, breakgain = breakgain, metric = metric)
-                      val ok =
-                        check(message_head, Protocol.message_heading(elem, pos)) &&
-                        check(message_body, XML.content(Pretty.unformatted(List(elem))))
-                      if (ok) buffer += message_text
-                    }
-                    if (buffer.nonEmpty) {
-                      progress.echo(thy_heading)
-                      buffer.foreach(progress.echo(_))
-                    }
-                  }
-              }
-            }
-
-            if (errors.nonEmpty) {
-              val msg = Symbol.output(unicode_symbols, cat_lines(errors))
-              progress.echo("\nBuild errors:\n" + Output.error_message_text(msg))
-            }
-            if (rc != Process_Result.RC.ok) {
-              progress.echo("\n" + Process_Result.RC.print_long(rc))
-            }
-        }
-      }
-    }
-
-    val errors = new mutable.ListBuffer[String]
-    for (session_name <- sessions) {
-      Exn.interruptible_capture(print(session_name)) match {
-        case Exn.Res(_) =>
-        case Exn.Exn(exn) => errors += Exn.message(exn)
-      }
-    }
-    if (errors.nonEmpty) error(cat_lines(errors.toList))
-  }
-
-
-  /* Isabelle tool wrapper */
-
-  val isabelle_tool = Isabelle_Tool("log", "print messages from build database",
-    Scala_Project.here,
-    { args =>
-      /* arguments */
-
-      var message_head = List.empty[Regex]
-      var message_body = List.empty[Regex]
-      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] [SESSIONS ...]
-
-  Options are:
-    -H REGEX     filter messages by matching against head
-    -M REGEX     filter messages by matching against body
-    -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 etc.
-
-  Print messages from the build database of the given sessions, without any
-  checks against current sources nor session structure: results from old
-  sessions or failed builds can be printed as well.
-
-  Multiple options -H and -M are conjunctive: all given patterns need to
-  match. Patterns match any substring, but ^ or $ may be used to match the
-  start or end explicitly.
-""",
-        "H:" -> (arg => message_head = message_head ::: List(arg.r)),
-        "M:" -> (arg => message_body = message_body ::: List(arg.r)),
-        "T:" -> (arg => theories = theories ::: List(arg)),
-        "U" -> (_ => unicode_symbols = true),
-        "m:" -> (arg => margin = Value.Double.parse(arg)),
-        "o:" -> (arg => options = options + arg),
-        "v" -> (_ => verbose = true))
-
-      val sessions = getopts(args)
-
-      val progress = new Console_Progress(verbose = verbose)
-
-      if (sessions.isEmpty) progress.echo_warning("No sessions to print")
-      else {
-        print_log(options, sessions, theories = theories, message_head = message_head,
-          message_body = message_body, margin = margin, progress = progress,
-          unicode_symbols = unicode_symbols)
-      }
-    })
 }