# HG changeset patch # User wenzelm # Date 1607541010 -3600 # Node ID cb0c407fbc6eb4eaf5e033e4ec5c26b55817081f # Parent a9e091ccd450d0cb3595919a94d31adb6d0a7c72 added "isabelle log": print messages from build database; diff -r a9e091ccd450 -r cb0c407fbc6e src/Pure/PIDE/rendering.scala --- 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 */ diff -r a9e091ccd450 -r cb0c407fbc6e src/Pure/System/isabelle_tool.scala --- 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, diff -r a9e091ccd450 -r cb0c407fbc6e src/Pure/Thy/sessions.scala --- 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]) diff -r a9e091ccd450 -r cb0c407fbc6e src/Pure/Tools/build_job.scala --- 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,