diff --git a/src/Pure/Thy/document_build.scala b/src/Pure/Thy/document_build.scala --- a/src/Pure/Thy/document_build.scala +++ b/src/Pure/Thy/document_build.scala @@ -1,545 +1,552 @@ /* Title: Pure/Thy/document_build.scala Author: Makarius Build theory document (PDF) from session database. */ package isabelle object Document_Build { /* document variants */ abstract class Document_Name { def name: String def path: Path = Path.basic(name) override def toString: String = name } object Document_Variant { def parse(opt: String): Document_Variant = Library.space_explode('=', opt) match { case List(name) => Document_Variant(name, Latex.Tags.empty) case List(name, tags) => Document_Variant(name, Latex.Tags(tags)) case _ => error("Malformed document variant: " + quote(opt)) } } sealed case class Document_Variant(name: String, tags: Latex.Tags) extends Document_Name { def print: String = if (tags.toString.isEmpty) name else name + "=" + tags.toString } sealed case class Document_Input(name: String, sources: SHA1.Digest) extends Document_Name { override def toString: String = name } sealed case class Document_Output(name: String, sources: SHA1.Digest, log_xz: Bytes, pdf: Bytes) extends Document_Name { override def toString: String = name def log: String = log_xz.uncompress().text def log_lines: List[String] = split_lines(log) def write(db: SQL.Database, session_name: String): Unit = write_document(db, session_name, this) def write(dir: Path): Path = { val path = dir + Path.basic(name).pdf Isabelle_System.make_directory(path.expand.dir) Bytes.write(path, pdf) path } } /* SQL data model */ object Data { val session_name = SQL.Column.string("session_name").make_primary_key val name = SQL.Column.string("name").make_primary_key val sources = SQL.Column.string("sources") val log_xz = SQL.Column.bytes("log_xz") val pdf = SQL.Column.bytes("pdf") val table = SQL.Table("isabelle_documents", List(session_name, name, sources, log_xz, pdf)) def where_equal(session_name: String, name: String = ""): SQL.Source = "WHERE " + Data.session_name.equal(session_name) + (if (name == "") "" else " AND " + Data.name.equal(name)) } def read_documents(db: SQL.Database, session_name: String): List[Document_Input] = { val select = Data.table.select(List(Data.name, Data.sources), Data.where_equal(session_name)) db.using_statement(select)(stmt => stmt.execute_query().iterator({ res => val name = res.string(Data.name) val sources = res.string(Data.sources) Document_Input(name, SHA1.fake_digest(sources)) }).toList) } def read_document( db: SQL.Database, session_name: String, name: String ): Option[Document_Output] = { val select = Data.table.select(sql = Data.where_equal(session_name, name)) db.using_statement(select)({ stmt => val res = stmt.execute_query() if (res.next()) { val name = res.string(Data.name) val sources = res.string(Data.sources) val log_xz = res.bytes(Data.log_xz) val pdf = res.bytes(Data.pdf) Some(Document_Output(name, SHA1.fake_digest(sources), log_xz, pdf)) } else None }) } def write_document(db: SQL.Database, session_name: String, doc: Document_Output): Unit = { db.using_statement(Data.table.insert()){ stmt => stmt.string(1) = session_name stmt.string(2) = doc.name stmt.string(3) = doc.sources.toString stmt.bytes(4) = doc.log_xz stmt.bytes(5) = doc.pdf stmt.execute() } } /* background context */ def session_background( options: Options, session: String, dirs: List[Path] = Nil, progress: Progress = new Progress, verbose: Boolean = false ): Sessions.Background = { Sessions.load_structure(options + "document=pdf", dirs = dirs). selection_deps(Sessions.Selection.session(session), progress = progress, verbose = verbose). background(session) } /* document context */ val texinputs: Path = Path.explode("~~/lib/texinputs") val isabelle_styles: List[Path] = List("isabelle.sty", "isabellesym.sty", "pdfsetup.sty", "railsetup.sty"). map(name => texinputs + Path.basic(name)) def context( session_context: Export.Session_Context, document_session: Option[Sessions.Base] = None, document_selection: Document.Node.Name => Boolean = _ => true, progress: Progress = new Progress ): Context = new Context(session_context, document_session, document_selection, progress) final class Context private[Document_Build]( val session_context: Export.Session_Context, document_session: Option[Sessions.Base], document_selection: Document.Node.Name => Boolean, val progress: Progress ) { context => /* session info */ private val base = document_session getOrElse session_context.session_base private val info = session_context.sessions_structure(base.session_name) def session: String = info.name def options: Options = info.options override def toString: String = session val classpath: List[File.Content] = session_context.classpath() def document_bibliography: Boolean = options.bool("document_bibliography") def document_logo: Option[String] = options.string("document_logo") match { case "" => None case "_" => Some("") case name => Some(name) } def document_build: String = options.string("document_build") def get_engine(): Engine = { val name = document_build Classpath(jar_contents = classpath).make_services(classOf[Engine]) .find(_.name == name).getOrElse(error("Bad document_build engine " + quote(name))) } /* document content */ def documents: List[Document_Variant] = info.documents def session_document_theories: List[Document.Node.Name] = base.proper_session_theories def all_document_theories: List[Document.Node.Name] = base.all_document_theories lazy val document_latex: List[File.Content_XML] = for (name <- all_document_theories) yield { val path = Path.basic(tex_name(name)) val content = if (document_selection(name)) { val entry = session_context(name.theory, Export.DOCUMENT_LATEX, permissive = true) YXML.parse_body(entry.text) } else Nil File.content(path, content) } lazy val session_graph: File.Content = { val path = Browser_Info.session_graph_path val content = graphview.Graph_File.make_pdf(options, base.session_graph_display) File.content(path, content) } lazy val session_tex: File.Content = { val path = Path.basic("session.tex") val content = Library.terminate_lines( session_document_theories.map(name => "\\input{" + tex_name(name) + "}")) File.content(path, content) } lazy val isabelle_logo: Option[File.Content] = { document_logo.map(logo_name => Isabelle_System.with_tmp_file("logo", ext = "pdf") { tmp_path => Logo.create_logo(logo_name, output_file = tmp_path, quiet = true) val path = Path.basic("isabelle_logo.pdf") val content = Bytes.read(tmp_path) File.content(path, content) }) } /* build document */ def build_document(doc: Document_Variant, verbose: Boolean = false): Document_Output = { Isabelle_System.with_tmp_dir("document") { tmp_dir => val engine = get_engine() val directory = engine.prepare_directory(context, tmp_dir, doc) engine.build_document(context, directory, verbose) } } /* document directory */ def make_directory(dir: Path, doc: Document_Variant): Path = Isabelle_System.make_directory(dir + Path.basic(doc.name)) def prepare_directory( dir: Path, doc: Document_Variant, latex_output: Latex.Output ): Directory = { val doc_dir = make_directory(dir, doc) /* actual sources: with SHA1 digest */ isabelle_styles.foreach(Isabelle_System.copy_file(_, doc_dir)) val comment_latex = latex_output.options.bool("document_comment_latex") if (!comment_latex) { Isabelle_System.copy_file(texinputs + Path.basic("comment.sty"), doc_dir) } doc.tags.sty(comment_latex).write(doc_dir) for ((base_dir, src) <- info.document_files) { Isabelle_System.copy_file_base(info.dir + base_dir, src, doc_dir) } session_tex.write(doc_dir) for (content <- document_latex) { content.output(latex_output(_, file_pos = content.path.implode_symbolic)) .write(doc_dir) } val root_name1 = "root_" + doc.name val root_name = if ((doc_dir + Path.explode(root_name1).tex).is_file) root_name1 else "root" val digests1 = List(doc.print, document_logo.toString, document_build).map(SHA1.digest) val digests2 = File.find_files(doc_dir.file, follow_links = true).map(SHA1.digest) val sources = SHA1.digest_set(digests1 ::: digests2) /* derived material: without SHA1 digest */ isabelle_logo.foreach(_.write(doc_dir)) session_graph.write(doc_dir) Directory(doc_dir, doc, root_name, sources) } def old_document(directory: Directory): Option[Document_Output] = for { db <- session_context.session_db() old_doc <- read_document(db, session, directory.doc.name) if old_doc.sources == directory.sources } yield old_doc } sealed case class Directory( doc_dir: Path, doc: Document_Variant, root_name: String, sources: SHA1.Digest ) { def root_name_script(ext: String = ""): String = Bash.string(if (ext.isEmpty) root_name else root_name + "." + ext) def conditional_script(ext: String, exe: String, after: String = ""): String = "if [ -f " + root_name_script(ext) + " ]\n" + "then\n" + " " + exe + " " + root_name_script() + "\n" + (if (after.isEmpty) "" else " " + after) + "fi\n" def log_errors(): List[String] = Latex.latex_errors(doc_dir, root_name) ::: Bibtex.bibtex_errors(doc_dir, root_name) def make_document(log: List[String], errors: List[String]): Document_Output = { val root_pdf = Path.basic(root_name).pdf val result_pdf = doc_dir + root_pdf if (errors.nonEmpty) { - val errors1 = errors ::: List("Failed to build document " + quote(doc.name)) - throw new Build_Error(log, Exn.cat_message(errors1: _*)) + val message = "Failed to build document " + quote(doc.name) + throw new Build_Error(log, errors ::: List(message)) } else if (!result_pdf.is_file) { val message = "Bad document result: expected to find " + root_pdf - throw new Build_Error(log, message) + throw new Build_Error(log, List(message)) } else { val log_xz = Bytes(cat_lines(log)).compress() val pdf = Bytes.read(result_pdf) Document_Output(doc.name, sources, log_xz, pdf) } } } /* build engines */ abstract class Engine(val name: String) extends Isabelle_System.Service { override def toString: String = name def prepare_directory(context: Context, dir: Path, doc: Document_Variant): Directory def build_document(context: Context, directory: Directory, verbose: Boolean): Document_Output } abstract class Bash_Engine(name: String) extends Engine(name) { def prepare_directory(context: Context, dir: Path, doc: Document_Variant): Directory = context.prepare_directory(dir, doc, new Latex.Output(context.options)) def use_pdflatex: Boolean = false def latex_script(context: Context, directory: Directory): String = (if (use_pdflatex) "$ISABELLE_PDFLATEX" else "$ISABELLE_LUALATEX") + " " + directory.root_name_script() + "\n" def bibtex_script(context: Context, directory: Directory, latex: Boolean = false): String = { val ext = if (context.document_bibliography) "aux" else "bib" directory.conditional_script(ext, "$ISABELLE_BIBTEX", after = if (latex) latex_script(context, directory) else "") } def makeindex_script(context: Context, directory: Directory, latex: Boolean = false): String = directory.conditional_script("idx", "$ISABELLE_MAKEINDEX", after = if (latex) latex_script(context, directory) else "") def use_build_script: Boolean = false def build_script(context: Context, directory: Directory): String = { val has_build_script = (directory.doc_dir + Path.explode("build")).is_file if (!use_build_script && has_build_script) { error("Unexpected document build script for option document_build=" + quote(context.document_build)) } else if (use_build_script && !has_build_script) error("Missing document build script") else if (has_build_script) "./build pdf " + Bash.string(directory.doc.name) else { "set -e\n" + latex_script(context, directory) + bibtex_script(context, directory, latex = true) + makeindex_script(context, directory) + latex_script(context, directory) + makeindex_script(context, directory, latex = true) } } def build_document( context: Context, directory: Directory, verbose: Boolean ): Document_Output = { val result = context.progress.bash( build_script(context, directory), cwd = directory.doc_dir.file, echo = verbose, watchdog = Time.seconds(0.5)) val log = result.out_lines ::: result.err_lines - val errors = (if (result.ok) Nil else List(result.err)) ::: directory.log_errors() - directory.make_document(log, errors) + val err = result.err + + val errors1 = directory.log_errors() + val errors2 = + if (result.ok) errors1 + else if (err.nonEmpty) err :: errors1 + else if (errors1.nonEmpty) errors1 + else List("Error") + directory.make_document(log, errors2) } } class LuaLaTeX_Engine extends Bash_Engine("lualatex") class PDFLaTeX_Engine extends Bash_Engine("pdflatex") { override def use_pdflatex: Boolean = true } class Build_Engine extends Bash_Engine("build") { override def use_build_script: Boolean = true } class LIPIcs_Engine(name: String) extends Bash_Engine(name) { def lipics_options(options: Options): Options = options + "document_heading_prefix=" + "document_comment_latex" override def use_pdflatex: Boolean = true override def prepare_directory(context: Context, dir: Path, doc: Document_Variant): Directory = { val doc_dir = context.make_directory(dir, doc) Build_LIPIcs.document_files.foreach(Isabelle_System.copy_file(_, doc_dir)) val latex_output = new Latex.Output(lipics_options(context.options)) context.prepare_directory(dir, doc, latex_output) } } class LIPIcs_LuaLaTeX_Engine extends LIPIcs_Engine("lipics") class LIPIcs_PDFLaTeX_Engine extends LIPIcs_Engine("lipics_pdflatex") { override def use_pdflatex: Boolean = true } /* build documents */ def tex_name(name: Document.Node.Name): String = name.theory_base_name + ".tex" - class Build_Error(val log_lines: List[String], val message: String) - extends Exn.User_Error(message) + class Build_Error(val log_lines: List[String], val log_errors: List[String]) + extends Exn.User_Error(Exn.cat_message(log_errors: _*)) def build_documents( context: Context, output_sources: Option[Path] = None, output_pdf: Option[Path] = None, verbose: Boolean = false ): List[Document_Output] = { val progress = context.progress val engine = context.get_engine() val documents = for (doc <- context.documents) yield { Isabelle_System.with_tmp_dir("document") { tmp_dir => progress.echo("Preparing " + context.session + "/" + doc.name + " ...") val start = Time.now() output_sources.foreach(engine.prepare_directory(context, _, doc)) val directory = engine.prepare_directory(context, tmp_dir, doc) val document = context.old_document(directory) getOrElse engine.build_document(context, directory, verbose) val stop = Time.now() val timing = stop - start progress.echo("Finished " + context.session + "/" + doc.name + " (" + timing.message_hms + " elapsed time)") document } } for (dir <- output_pdf; doc <- documents) { val path = doc.write(dir) progress.echo("Document at " + path.absolute) } documents } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("document", "prepare session theory document", Scala_Project.here, { args => var output_sources: Option[Path] = None var output_pdf: Option[Path] = None var verbose_latex = false var dirs: List[Path] = Nil var options = Options.init() var verbose_build = false val getopts = Getopts(""" Usage: isabelle document [OPTIONS] SESSION Options are: -O DIR output directory for LaTeX sources and resulting PDF -P DIR output directory for resulting PDF -S DIR output directory for LaTeX sources -V verbose latex -d DIR include session directory -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -v verbose build Prepare the theory document of a session. """, "O:" -> (arg => { val dir = Path.explode(arg) output_sources = Some(dir) output_pdf = Some(dir) }), "P:" -> (arg => { output_pdf = Some(Path.explode(arg)) }), "S:" -> (arg => { output_sources = Some(Path.explode(arg)) }), "V" -> (_ => verbose_latex = true), "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), "o:" -> (arg => options = options + arg), "v" -> (_ => verbose_build = true)) val more_args = getopts(args) val session = more_args match { case List(a) => a case _ => getopts.usage() } val progress = new Console_Progress(verbose = verbose_build) progress.interrupt_handler { val build_results = Build.build(options, selection = Sessions.Selection.session(session), dirs = dirs, progress = progress, verbose = verbose_build) if (!build_results.ok) error("Failed to build session " + quote(session)) if (output_sources.isEmpty && output_pdf.isEmpty) { progress.echo_warning("No output directory") } val session_background = Document_Build.session_background(options, session, dirs = dirs) using(Export.open_session_context(build_results.store, session_background)) { session_context => build_documents( context(session_context, progress = progress), output_sources = output_sources, output_pdf = output_pdf, verbose = verbose_latex) } } }) } diff --git a/src/Pure/Tools/build_job.scala b/src/Pure/Tools/build_job.scala --- a/src/Pure/Tools/build_job.scala +++ b/src/Pure/Tools/build_job.scala @@ -1,579 +1,579 @@ /* Title: Pure/Tools/build_job.scala Author: Makarius Build job running prover process, with rudimentary PIDE session. */ package isabelle import scala.collection.mutable import scala.util.matching.Regex object Build_Job { /* theory markup/messages from session database */ def read_theory( theory_context: Export.Theory_Context, unicode_symbols: Boolean = false ): Option[Document.Snapshot] = { def read(name: String): Export.Entry = theory_context(name, permissive = true) def read_xml(name: String): XML.Body = YXML.parse_body( Symbol.output(unicode_symbols, UTF8.decode_permissive(read(name).uncompressed)), cache = theory_context.cache) for { id <- theory_context.document_id() (thy_file, blobs_files) <- theory_context.files(permissive = true) } yield { val master_dir = Thy_Header.split_file_name(thy_file) match { case Some((dir, _)) => dir case None => error("Cannot determine theory master directory: " + quote(thy_file)) } val node_name = Document.Node.Name(thy_file, master_dir = master_dir, theory = theory_context.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 name = Document.Node.Name(file) val path = Path.explode(file) val src_path = File.relative_path(node_name.master_dir_path, path).getOrElse(path) Command.Blob(name, src_path, None) } val blobs_xml = for (i <- (1 to blobs.length).toList) yield read_xml(Export.MARKUP + i) 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 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, 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, blobs_info = blobs_info, results = results, markups = markups) Document.State.init.snippet(command) } } /* print messages */ def print_log( options: Options, sessions: List[String], theories: List[String] = Nil, message_head: List[Regex] = Nil, message_body: List[Regex] = Nil, verbose: Boolean = false, 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 => verbose || Protocol.is_exported(message.info)) if (messages.nonEmpty) { val line_document = Line.Document(snapshot.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() 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, verbose = verbose, margin = margin, progress = progress, unicode_symbols = unicode_symbols) } }) } class Build_Job(progress: Progress, session_background: Sessions.Background, store: Sessions.Store, do_store: Boolean, log: Logger, session_setup: (String, Session) => Unit, val numa_node: Option[Int], command_timings0: List[Properties.T] ) { def session_name: String = session_background.session_name val info: Sessions.Info = session_background.sessions_structure(session_name) val options: Options = NUMA.policy_options(info.options, numa_node) private val future_result: Future[Process_Result] = Future.thread("build", uninterruptible = true) { val parent = info.parent.getOrElse("") val env = Isabelle_System.settings( List("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString)) val is_pure = Sessions.is_pure(session_name) val use_prelude = if (is_pure) Thy_Header.ml_roots.map(_._1) else Nil val eval_store = if (do_store) { (if (info.theories.nonEmpty) List("ML_Heap.share_common_data ()") else Nil) ::: List("ML_Heap.save_child " + ML_Syntax.print_string_bytes(File.platform_path(store.output_heap(session_name)))) } else Nil val resources = new Resources(session_background, log = log, command_timings = command_timings0) val session = new Session(options, resources) { override val cache: Term.Cache = store.cache override def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info = { val name1 = name.map(s => Path.explode(s).expand.implode) session_background.base.load_commands.get(name1) match { case Some(spans) => val syntax = session_background.base.theory_syntax(name) Command.build_blobs_info(syntax, name, spans) case None => Command.Blobs_Info.none } } } object Build_Session_Errors { private val promise: Promise[List[String]] = Future.promise def result: Exn.Result[List[String]] = promise.join_result def cancel(): Unit = promise.cancel() def apply(errs: List[String]): Unit = { try { promise.fulfill(errs) } catch { case _: IllegalStateException => } } } val export_consumer = Export.consumer(store.open_database(session_name, output = true), store.cache, progress = progress) val stdout = new StringBuilder(1000) val stderr = new StringBuilder(1000) val command_timings = new mutable.ListBuffer[Properties.T] val theory_timings = new mutable.ListBuffer[Properties.T] val session_timings = new mutable.ListBuffer[Properties.T] val runtime_statistics = new mutable.ListBuffer[Properties.T] val task_statistics = new mutable.ListBuffer[Properties.T] def fun( name: String, acc: mutable.ListBuffer[Properties.T], unapply: Properties.T => Option[Properties.T] ): (String, Session.Protocol_Function) = { name -> ((msg: Prover.Protocol_Output) => unapply(msg.properties) match { case Some(props) => acc += props; true case _ => false }) } session.init_protocol_handler(new Session.Protocol_Handler { override def exit(): Unit = Build_Session_Errors.cancel() private def build_session_finished(msg: Prover.Protocol_Output): Boolean = { val (rc, errors) = try { val (rc, errs) = { import XML.Decode._ pair(int, list(x => x))(Symbol.decode_yxml(msg.text)) } val errors = for (err <- errs) yield { val prt = Protocol_Message.expose_no_reports(err) Pretty.string_of(prt, metric = Symbol.Metric) } (rc, errors) } catch { case ERROR(err) => (Process_Result.RC.failure, List(err)) } session.protocol_command("Prover.stop", rc.toString) Build_Session_Errors(errors) true } private def loading_theory(msg: Prover.Protocol_Output): Boolean = msg.properties match { case Markup.Loading_Theory(Markup.Name(name)) => progress.theory(Progress.Theory(name, session = session_name)) false case _ => false } private def export_(msg: Prover.Protocol_Output): Boolean = msg.properties match { case Protocol.Export(args) => export_consumer.make_entry(session_name, args, msg.chunk) true case _ => false } override val functions: Session.Protocol_Functions = List( Markup.Build_Session_Finished.name -> build_session_finished, Markup.Loading_Theory.name -> loading_theory, Markup.EXPORT -> export_, fun(Markup.Theory_Timing.name, theory_timings, Markup.Theory_Timing.unapply), fun(Markup.Session_Timing.name, session_timings, Markup.Session_Timing.unapply), fun(Markup.Task_Statistics.name, task_statistics, Markup.Task_Statistics.unapply)) }) session.command_timings += Session.Consumer("command_timings") { case Session.Command_Timing(props) => for { elapsed <- Markup.Elapsed.unapply(props) elapsed_time = Time.seconds(elapsed) if elapsed_time.is_relevant && elapsed_time >= options.seconds("command_timing_threshold") } command_timings += props.filter(Markup.command_timing_property) } session.runtime_statistics += Session.Consumer("ML_statistics") { case Session.Runtime_Statistics(props) => runtime_statistics += props } session.finished_theories += Session.Consumer[Document.Snapshot]("finished_theories") { case snapshot => if (!progress.stopped) { val rendering = new Rendering(snapshot, options, session) def export_(name: String, xml: XML.Body, compress: Boolean = true): Unit = { if (!progress.stopped) { val theory_name = snapshot.node_name.theory val args = Protocol.Export.Args(theory_name = theory_name, name = name, compress = compress) val body = Bytes(Symbol.encode(YXML.string_of_body(xml))) export_consumer.make_entry(session_name, args, body) } } def export_text(name: String, text: String, compress: Boolean = true): Unit = export_(name, List(XML.Text(text)), compress = compress) for (command <- snapshot.snippet_command) { export_text(Export.DOCUMENT_ID, command.id.toString, compress = false) } export_text(Export.FILES, cat_lines(snapshot.node_files.map(_.path.implode_symbolic)), compress = false) for (((_, xml), i) <- snapshot.xml_markup_blobs().zipWithIndex) { export_(Export.MARKUP + (i + 1), xml) } export_(Export.MARKUP, snapshot.xml_markup()) export_(Export.MESSAGES, snapshot.messages.map(_._1)) val citations = Library.distinct(rendering.citations(Text.Range.full).map(_.info)) export_text(Export.DOCUMENT_CITATIONS, cat_lines(citations)) } } session.all_messages += Session.Consumer[Any]("build_session_output") { case msg: Prover.Output => val message = msg.message if (msg.is_system) resources.log(Protocol.message_text(message)) if (msg.is_stdout) { stdout ++= Symbol.encode(XML.content(message)) } else if (msg.is_stderr) { stderr ++= Symbol.encode(XML.content(message)) } else if (msg.is_exit) { val err = "Prover terminated" + (msg.properties match { case Markup.Process_Result(result) => ": " + result.print_rc case _ => "" }) Build_Session_Errors(List(err)) } case _ => } session_setup(session_name, session) val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store) val process = Isabelle_Process.start(store, options, session, session_background, logic = parent, raw_ml_system = is_pure, use_prelude = use_prelude, eval_main = eval_main, cwd = info.dir.file, env = env) val build_errors = Isabelle_Thread.interrupt_handler(_ => process.terminate()) { Exn.capture { process.await_startup() } match { case Exn.Res(_) => val resources_yxml = resources.init_session_yxml val encode_options: XML.Encode.T[Options] = options => session.prover_options(options).encode val args_yxml = YXML.string_of_body( { import XML.Encode._ pair(string, list(pair(encode_options, list(pair(string, properties)))))( (session_name, info.theories)) }) session.protocol_command("build_session", resources_yxml, args_yxml) Build_Session_Errors.result case Exn.Exn(exn) => Exn.Res(List(Exn.message(exn))) } } val process_result = Isabelle_Thread.interrupt_handler(_ => process.terminate()) { process.await_shutdown() } session.stop() val export_errors = export_consumer.shutdown(close = true).map(Output.error_message_text) val (document_output, document_errors) = try { if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && info.documents.nonEmpty) { using(Export.open_database_context(store)) { database_context => val documents = using(database_context.open_session(session_background)) { session_context => Document_Build.build_documents( Document_Build.context(session_context, progress = progress), output_sources = info.document_output, output_pdf = info.document_output) } using(database_context.open_database(session_name, output = true))(session_database => documents.foreach(_.write(session_database.db, session_name))) (documents.flatMap(_.log_lines), Nil) } } else (Nil, Nil) } catch { - case exn: Document_Build.Build_Error => (exn.log_lines, List(exn.message)) + case exn: Document_Build.Build_Error => (exn.log_lines, exn.log_errors) case Exn.Interrupt.ERROR(msg) => (Nil, List(msg)) } val result = { val theory_timing = theory_timings.iterator.flatMap( { case props @ Markup.Name(name) => Some(name -> props) case _ => None }).toMap val used_theory_timings = for { (name, _) <- session_background.base.used_theories } yield theory_timing.getOrElse(name.theory, Markup.Name(name.theory)) val more_output = Library.trim_line(stdout.toString) :: 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) ::: runtime_statistics.toList.map(Protocol.ML_Statistics_Marker.apply) ::: task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply) ::: document_output process_result.output(more_output) .error(Library.trim_line(stderr.toString)) .errors_rc(export_errors ::: document_errors) } build_errors match { case Exn.Res(build_errs) => val errs = build_errs ::: document_errors if (errs.nonEmpty) { result.error_rc.output( errs.flatMap(s => split_lines(Output.error_message_text(s))) ::: errs.map(Protocol.Error_Message_Marker.apply)) } else if (progress.stopped && result.ok) result.copy(rc = Process_Result.RC.interrupt) else result case Exn.Exn(Exn.Interrupt()) => if (result.ok) result.copy(rc = Process_Result.RC.interrupt) else result case Exn.Exn(exn) => throw exn } } def terminate(): Unit = future_result.cancel() def is_finished: Boolean = future_result.is_finished private val timeout_request: Option[Event_Timer.Request] = { if (info.timeout_ignored) None else Some(Event_Timer.request(Time.now() + info.timeout) { terminate() }) } def join: (Process_Result, Option[String]) = { val result1 = future_result.join val was_timeout = timeout_request match { case None => false case Some(request) => !request.cancel() } val result2 = if (result1.ok) result1 else if (was_timeout) result1.error(Output.error_message_text("Timeout")).timeout_rc else if (result1.interrupted) result1.error(Output.error_message_text("Interrupt")) else result1 val heap_digest = if (result2.ok && do_store && store.output_heap(session_name).is_file) Some(Sessions.write_heap_digest(store.output_heap(session_name))) else None (result2, heap_digest) } } diff --git a/src/Tools/jEdit/src/document_dockable.scala b/src/Tools/jEdit/src/document_dockable.scala --- a/src/Tools/jEdit/src/document_dockable.scala +++ b/src/Tools/jEdit/src/document_dockable.scala @@ -1,362 +1,366 @@ /* Title: Tools/jEdit/src/document_dockable.scala Author: Makarius Dockable window for document build support. */ package isabelle.jedit import isabelle._ import java.awt.BorderLayout import java.awt.event.{ComponentEvent, ComponentAdapter} import scala.swing.{ScrollPane, TextArea, Label, TabbedPane, BorderPanel, Component} import scala.swing.event.SelectionChanged import org.gjt.sp.jedit.{jEdit, View} object Document_Dockable { /* state */ object Status extends Enumeration { val WAITING = Value("waiting") val RUNNING = Value("running") val FINISHED = Value("finished") } object State { def init(): State = State() } sealed case class State( progress: Progress = new Progress, process: Future[Unit] = Future.value(()), status: Status.Value = Status.FINISHED, output: List[XML.Tree] = Nil ) { def run(progress: Progress, process: Future[Unit]): State = copy(progress = progress, process = process, status = Status.RUNNING) def finish(output: List[XML.Tree]): State = copy(process = Future.value(()), status = Status.FINISHED, output = output) def ok: Boolean = !output.exists(Protocol.is_error) } } class Document_Dockable(view: View, position: String) extends Dockable(view, position) { dockable => GUI_Thread.require {} /* component state -- owned by GUI thread */ private val current_state = Synchronized(Document_Dockable.State.init()) private val process_indicator = new Process_Indicator private val pretty_text_area = new Pretty_Text_Area(view) private val message_pane = new TabbedPane private def show_state(): Unit = GUI_Thread.later { val st = current_state.value pretty_text_area.update(Document.Snapshot.init, Command.Results.empty, st.output) st.status match { case Document_Dockable.Status.WAITING => process_indicator.update("Waiting for PIDE document content ...", 5) case Document_Dockable.Status.RUNNING => process_indicator.update("Running document build process ...", 15) case Document_Dockable.Status.FINISHED => process_indicator.update(null, 0) } } private def show_page(page: TabbedPane.Page): Unit = GUI_Thread.later { message_pane.selection.page = page } /* text area with zoom/resize */ override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() } private def handle_resize(): Unit = GUI_Thread.require { pretty_text_area.zoom(zoom) } private val delay_resize: Delay = Delay.first(PIDE.session.update_delay, gui = true) { handle_resize() } addComponentListener(new ComponentAdapter { override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke() override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke() }) /* progress log */ private val log_area = new TextArea { editable = false font = GUI.copy_font((new Label).font) } private val scroll_log_area = new ScrollPane(log_area) def log_progress(): Document_Editor.Log_Progress = new Document_Editor.Log_Progress(PIDE.session) { override def show(text: String): Unit = if (text != log_area.text) { log_area.text = text val vertical = scroll_log_area.peer.getVerticalScrollBar vertical.setValue(vertical.getMaximum) } } /* document build process */ private def init_state(): Unit = current_state.change { _ => Document_Dockable.State(progress = log_progress()) } private def cancel_process(): Unit = current_state.change { st => st.process.cancel(); st } private def await_process(): Unit = current_state.guarded_access(st => if (st.process.is_finished) None else Some((), st)) private def finish_process(output: List[XML.Tree]): Unit = current_state.change(_.finish(output)) private def run_process(body: Document_Editor.Log_Progress => Unit): Boolean = { val started = current_state.change_result { st => if (st.process.is_finished) { val progress = log_progress() val process = Future.thread[Unit](name = "Document_Dockable.process") { await_process() body(progress) } (true, st.run(progress, process)) } else (false, st) } show_state() started } private def load_document(session: String): Boolean = { val options = PIDE.options.value run_process { _ => try { val session_background = Document_Build.session_background( options, session, dirs = JEdit_Sessions.session_dirs) PIDE.editor.document_setup(Some(session_background)) finish_process(Nil) GUI_Thread.later { refresh_theories() show_state() show_page(theories_page) } } catch { case exn: Throwable if !Exn.is_interrupt(exn) => finish_process(List(Protocol.error_message(Exn.print(exn)))) GUI_Thread.later { show_state() show_page(output_page) } } } } private def document_build( session_background: Sessions.Background, progress: Document_Editor.Log_Progress ): Unit = { val store = JEdit_Sessions.sessions_store(PIDE.options.value) val document_selection = PIDE.editor.document_selection() val snapshot = PIDE.session.await_stable_snapshot() val session_context = Export.open_session_context(store, session_background, document_snapshot = Some(snapshot)) try { val context = Document_Build.context(session_context, document_session = Some(session_background.base), document_selection = document_selection, progress = progress) val variant = session_background.info.documents.head Isabelle_System.make_directory(Document_Editor.document_output_dir()) val doc = context.build_document(variant, verbose = true) // log File.write(Document_Editor.document_output().log, doc.log) GUI_Thread.later { progress.finish(doc.log) } // pdf Bytes.write(Document_Editor.document_output().pdf, doc.pdf) Document_Editor.view_document() } finally { session_context.close() } } private def build_document(): Unit = { PIDE.editor.document_session() match { case Some(session_background) if session_background.info.documents.nonEmpty => run_process { progress => show_page(log_page) - val res = Exn.capture { document_build(session_background, progress) } - val msg = - res match { - case Exn.Res(_) => Protocol.writeln_message("OK") - case Exn.Exn(exn) => Protocol.error_message(Exn.print(exn)) + val result = Exn.capture { document_build(session_background, progress) } + val msgs = + result match { + case Exn.Res(_) => + List(Protocol.writeln_message("OK")) + case Exn.Exn(exn: Document_Build.Build_Error) => + exn.log_errors.map(s => Protocol.error_message(YXML.parse_body(s))) + case Exn.Exn(exn) => + List(Protocol.error_message(YXML.parse_body(Exn.print(exn)))) } - finish_process(List(msg)) + finish_process(Pretty.separate(msgs)) show_state() - show_page(if (Exn.is_interrupt_exn(res)) theories_page else output_page) + show_page(if (Exn.is_interrupt_exn(result)) theories_page else output_page) } case _ => } } /* controls */ private val document_session = JEdit_Sessions.document_selector(PIDE.options, standalone = true) private lazy val delay_load: Delay = Delay.last(PIDE.session.load_delay, gui = true) { for (session <- document_session.selection_value) { if (!load_document(session)) delay_load.invoke() } } document_session.reactions += { case SelectionChanged(_) => delay_load.invoke() } private val load_button = new GUI.Button("Load") { tooltip = "Load document theories" override def clicked(): Unit = PIDE.editor.document_select_all(set = true) } private val build_button = new GUI.Button("Build") { tooltip = "Build document" override def clicked(): Unit = build_document() } private val cancel_button = new GUI.Button("Cancel") { tooltip = "Cancel build process" override def clicked(): Unit = cancel_process() } private val view_button = new GUI.Button("View") { tooltip = "View document" override def clicked(): Unit = Document_Editor.view_document() } private val controls = Wrap_Panel(List(document_session, process_indicator.component, load_button, build_button, view_button, cancel_button)) add(controls.peer, BorderLayout.NORTH) override def focusOnDefaultComponent(): Unit = build_button.requestFocus() /* message pane with pages */ private val reset_button = new GUI.Button("Reset") { tooltip = "Deselect document theories" override def clicked(): Unit = PIDE.editor.document_select_all(set = false) } private val purge_button = new GUI.Button("Purge") { tooltip = "Remove theories that are no longer required" override def clicked(): Unit = PIDE.editor.purge() } private val theories_controls = Wrap_Panel(List(reset_button, purge_button)) private val theories = new Theories_Status(view, document = true) private def refresh_theories(): Unit = { val domain = PIDE.editor.document_theories().toSet theories.update(domain = Some(domain), trim = true, force = true) theories.refresh() } private val theories_page = new TabbedPane.Page("Theories", new BorderPanel { layout(theories_controls) = BorderPanel.Position.North layout(theories.gui) = BorderPanel.Position.Center }, "Selection and status of document theories") private val output_controls = Wrap_Panel(List(pretty_text_area.search_label, pretty_text_area.search_field, zoom)) private val output_page = new TabbedPane.Page("Output", new BorderPanel { layout(output_controls) = BorderPanel.Position.North layout(Component.wrap(pretty_text_area)) = BorderPanel.Position.Center }, "Output from build process") private val log_page = new TabbedPane.Page("Log", new BorderPanel { layout(scroll_log_area) = BorderPanel.Position.Center }, "Raw log of build process") message_pane.pages ++= List(theories_page, log_page, output_page) set_content(message_pane) /* main */ private val main = Session.Consumer[Any](getClass.getName) { case _: Session.Global_Options => GUI_Thread.later { document_session.load() handle_resize() refresh_theories() } case changed: Session.Commands_Changed => GUI_Thread.later { val domain = PIDE.editor.document_theories().filter(changed.nodes).toSet if (domain.nonEmpty) theories.update(domain = Some(domain)) } } override def init(): Unit = { PIDE.editor.document_init(dockable) init_state() PIDE.session.global_options += main PIDE.session.commands_changed += main handle_resize() delay_load.invoke() } override def exit(): Unit = { PIDE.session.global_options -= main PIDE.session.commands_changed -= main delay_resize.revoke() PIDE.editor.document_exit(dockable) } }