--- 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)
- }
- })
}