--- a/src/Pure/PIDE/rendering.scala Wed Dec 09 15:53:45 2020 +0100
+++ b/src/Pure/PIDE/rendering.scala Wed Dec 09 20:10:10 2020 +0100
@@ -211,6 +211,7 @@
Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR,
Markup.BAD)
+ val message_elements = Markup.Elements(message_pri.keySet)
val warning_elements = Markup.Elements(Markup.WARNING, Markup.LEGACY)
val error_elements = Markup.Elements(Markup.ERROR)
@@ -520,7 +521,7 @@
}
- /* message underline color */
+ /* messages */
def message_underline_color(elements: Markup.Elements, range: Text.Range)
: List[Text.Info[Rendering.Color.Value]] =
@@ -536,6 +537,39 @@
} yield Text.Info(r, color)
}
+ def text_messages(range: Text.Range): List[Text.Info[XML.Tree]] =
+ {
+ val results =
+ snapshot.cumulate[Vector[XML.Tree]](range, Vector.empty, Rendering.message_elements,
+ 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
+ }
+ case _ => None
+ })
+
+ 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
+ }
+ for {
+ Text.Info(range, trees) <- results
+ tree <- trees
+ if !seen(tree)
+ } yield Text.Info(range, tree)
+ }
+
/* tooltips */
--- a/src/Pure/System/isabelle_tool.scala Wed Dec 09 15:53:45 2020 +0100
+++ b/src/Pure/System/isabelle_tool.scala Wed Dec 09 20:10:10 2020 +0100
@@ -182,6 +182,7 @@
class Tools extends Isabelle_Scala_Tools(
Build.isabelle_tool,
Build_Docker.isabelle_tool,
+ Build_Job.isabelle_tool,
Doc.isabelle_tool,
Dump.isabelle_tool,
Export.isabelle_tool,
--- a/src/Pure/Thy/sessions.scala Wed Dec 09 15:53:45 2020 +0100
+++ b/src/Pure/Thy/sessions.scala Wed Dec 09 20:10:10 2020 +0100
@@ -635,6 +635,8 @@
object Structure
{
+ val empty: Structure = make(Nil)
+
def make(infos: List[Info]): Structure =
{
def add_edges(graph: Graph[String, Info], kind: String, edges: Info => Traversable[String])
--- a/src/Pure/Tools/build_job.scala Wed Dec 09 15:53:45 2020 +0100
+++ b/src/Pure/Tools/build_job.scala Wed Dec 09 20:10:10 2020 +0100
@@ -66,6 +66,104 @@
case _ => None
}
}
+
+
+ /* print messages */
+
+ def print_log(
+ options: Options,
+ session_name: String,
+ theories: List[String] = Nil,
+ progress: Progress = new Progress,
+ margin: Double = Pretty.default_margin,
+ breakgain: Double = Pretty.default_breakgain,
+ metric: Pretty.Metric = Pretty.Default_Metric)
+ {
+ val store = Sessions.store(options)
+
+ val resources = new Resources(Sessions.Structure.empty, Sessions.Structure.empty.bootstrap)
+ val session = new Session(options, resources)
+
+ using(store.open_database_context())(db_context =>
+ {
+ val result =
+ db_context.input_database(session_name)((db, _) =>
+ {
+ val theories = store.read_theories(db, session_name)
+ val errors = store.read_errors(db, session_name)
+ store.read_build(db, session_name).map(info => (theories, errors, info.return_code))
+ })
+ result match {
+ case None => error("Missing build database for session " + quote(session_name))
+ case Some((used_theories, errors, rc)) =>
+ val bad_theories = theories.filterNot(used_theories.toSet)
+ if (bad_theories.nonEmpty) error("Unknown theories " + commas_quote(bad_theories))
+
+ 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")
+ case Some(command) =>
+ progress.echo(thy_heading)
+ val snapshot = Document.State.init.snapshot().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))
+ }
+ }
+ }
+
+ if (errors.nonEmpty) {
+ progress.echo("\nErrors:\n" + Output.error_message_text(cat_lines(errors)))
+ }
+ if (rc != 0) progress.echo("\n" + Process_Result.print_return_code(rc))
+ }
+ })
+ }
+
+
+ /* Isabelle tool wrapper */
+
+ val isabelle_tool = Isabelle_Tool("log", "print messages from build database",
+ Scala_Project.here, args =>
+ {
+ /* arguments */
+
+ var theories: List[String] = Nil
+ var margin = Pretty.default_margin
+ var options = Options.init()
+
+ val getopts = Getopts("""
+Usage: isabelle log [OPTIONS] SESSION
+
+ Options are:
+ -T NAME restrict to given theories (multiple options)
+ -m MARGIN margin for pretty printing (default: """ + margin + """)
+ -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.
+""",
+ "T:" -> (arg => theories = theories ::: List(arg)),
+ "m:" -> (arg => margin = Value.Double.parse(arg)),
+ "o:" -> (arg => options = options + arg))
+
+ val more_args = getopts(args)
+ val session_name =
+ more_args match {
+ case List(session_name) => session_name
+ case _ => getopts.usage()
+ }
+
+ val progress = new Console_Progress()
+
+ print_log(options, session_name, theories = theories, margin = margin, progress = progress)
+ })
}
class Build_Job(progress: Progress,