diff --git a/src/Pure/Thy/browser_info.scala b/src/Pure/Thy/browser_info.scala --- a/src/Pure/Thy/browser_info.scala +++ b/src/Pure/Thy/browser_info.scala @@ -1,704 +1,703 @@ /* Title: Pure/Thy/browser_info.scala Author: Makarius HTML/PDF presentation of PIDE document information. */ package isabelle import scala.annotation.tailrec import scala.collection.immutable.SortedMap import scala.collection.mutable object Browser_Info { /* browser_info store configuration */ object Config { val none: Config = new Config { def enabled: Boolean = false } val standard: Config = new Config { def enabled: Boolean = true } def dir(path: Path): Config = new Config { def enabled: Boolean = true override def presentation_dir(store: Sessions.Store): Path = path } def make(s: String): Config = if (s == ":") standard else dir(Path.explode(s)) } abstract class Config private { def enabled: Boolean def enabled(info: Sessions.Info): Boolean = enabled || info.browser_info def presentation_dir(store: Sessions.Store): Path = store.presentation_dir } /* meta data within the file-system */ object Meta_Data { /* directory */ val PATH: Path = Path.explode(".browser_info") def check_directory(dir: Path): Unit = { if (dir.is_dir && !(dir + PATH).is_dir && File.read_dir(dir).nonEmpty) { error("Existing content in " + dir.expand + " lacks " + PATH + " meta data.\n" + "To avoid potential disaster, it has not been changed automatically.\n" + "If this is the intended directory, please move/remove/empty it manually.") } } def init_directory(dir: Path): Path = { check_directory(dir) Isabelle_System.make_directory(dir + PATH) dir } def clean_directory(dir: Path): Path = { check_directory(dir) Isabelle_System.rm_tree(dir) // guarded by check_directory! Isabelle_System.new_directory(dir + PATH) } /* content */ def make_path(dir: Path, name: String): Path = dir + PATH + Path.basic(name) def value(dir: Path, name: String): String = { val path = make_path(dir, name) if (path.is_file) File.read(path) else "" } def change(dir: Path, name: String)(f: String => String): Unit = { val path = make_path(dir, name) val x = value(dir, name) val y = try { f(x) } catch { case ERROR(msg) => error("Failed to change " + path.expand + ":\n" + msg)} if (x != y) File.write(path, y) } /* build_uuid */ val BUILD_UUID = "build_uuid" def check_build_uuid(dir: Path, uuid: String): Boolean = { val uuid0 = value(dir, BUILD_UUID) uuid0.nonEmpty && uuid.nonEmpty && uuid0 == uuid } def set_build_uuid(dir: Path, uuid: String): Unit = change(dir, BUILD_UUID)(_ => uuid) /* index */ val INDEX = "index.json" object Item { def parse(json: JSON.T): Item = { def err(): Nothing = error("Bad JSON object for item:\n" + JSON.Format.pretty_print(json)) val obj = JSON.Object.unapply(json) getOrElse err() val name = JSON.string(obj, "name") getOrElse err() val description = JSON.string(obj, "description") getOrElse "" Item(name, description = Symbol.trim_blank_lines(description)) } } sealed case class Item(name: String, description: String = "") { override def toString: String = name def json: JSON.T = JSON.Object("name" -> name, "description" -> description) } object Index { def parse(s: JSON.S, kind: String): Index = { if (s.isEmpty) Index(kind, Nil) else { def err(): Nothing = error("Bad JSON object " + kind + " index:\n" + s) val json = JSON.parse(s) val obj = JSON.Object.unapply(json) getOrElse err() val kind1 = JSON.string(obj, "kind") getOrElse err() val items = JSON.list(obj, "items", x => Some(Item.parse(x))) getOrElse err() if (kind == kind1) Index(kind, items) else error("Expected index kind " + quote(kind) + " but found " + quote(kind1)) } } } sealed case class Index(kind: String, items: List[Item]) { def is_empty: Boolean = items.isEmpty def + (item: Item): Index = Index(kind, (item :: items.filterNot(_.name == item.name)).sortBy(_.name)) def json: JSON.T = JSON.Object("kind" -> kind, "items" -> items.map(_.json)) def print_json: JSON.S = JSON.Format.pretty_print(json) } } /* presentation elements */ sealed case class Elements( html: Markup.Elements = Markup.Elements.empty, entity: Markup.Elements = Markup.Elements.empty, language: Markup.Elements = Markup.Elements.empty) val default_elements: Elements = Elements( html = Rendering.foreground_elements ++ Rendering.text_color_elements + Markup.NUMERAL + Markup.COMMENT + Markup.ENTITY + Markup.LANGUAGE + Markup.PATH + Markup.URL, entity = Markup.Elements(Markup.THEORY, Markup.TYPE_NAME, Markup.CONSTANT, Markup.FACT, Markup.CLASS, Markup.LOCALE, Markup.FREE)) val extra_elements: Elements = Elements( html = default_elements.html ++ Rendering.markdown_elements, language = Markup.Elements(Markup.Language.DOCUMENT)) /** HTML/PDF presentation context **/ def context( sessions_structure: Sessions.Structure, elements: Elements = default_elements, root_dir: Path = Path.current, document_info: Document_Info = Document_Info.empty ): Context = new Context(sessions_structure, elements, root_dir, document_info) class Context private[Browser_Info]( sessions_structure: Sessions.Structure, val elements: Elements, val root_dir: Path, val document_info: Document_Info ) { /* directory structure and resources */ def theory_by_name(session: String, theory: String): Option[Document_Info.Theory] = document_info.theory_by_name(session, theory) def theory_by_file(session: String, file: String): Option[Document_Info.Theory] = document_info.theory_by_file(session, file) def session_chapter(session: String): String = sessions_structure(session).chapter def chapter_dir(session: String): Path = root_dir + Path.basic(session_chapter(session)) def session_dir(session: String): Path = chapter_dir(session) + Path.basic(session) def theory_dir(theory: Document_Info.Theory): Path = session_dir(theory.dynamic_session) def theory_html(theory: Document_Info.Theory): Path = { def check(name: String): Option[Path] = { val path = Path.basic(name).html if (Path.eq_case_insensitive(path, Path.index_html)) None else Some(path) } check(theory.print_short) orElse check(theory.name) getOrElse error("Illegal global theory name " + quote(theory.name) + " (conflict with " + Path.index_html + ")") } def file_html(file: String): Path = Path.explode(file).squash.html def smart_html(theory: Document_Info.Theory, file: String): Path = if (File.is_thy(file)) theory_html(theory) else file_html(file) /* HTML content */ def head(title: String, rest: XML.Body = Nil): XML.Tree = HTML.div("head", HTML.chapter(title) :: rest) def source(body: XML.Body): XML.Tree = HTML.pre("source", body) def contents( heading: String, items: List[XML.Body], css_class: String = "contents" ) : List[XML.Elem] = { if (items.isEmpty) Nil else List(HTML.div(css_class, List(HTML.section(heading), HTML.itemize(items)))) } /* preview PIDE document */ lazy val isabelle_css: String = File.read(HTML.isabelle_css) def html_document(title: String, body: XML.Body, fonts_css: String): HTML_Document = { val content = HTML.output_document( List( HTML.style(fonts_css + "\n\n" + isabelle_css), HTML.title(title)), List(HTML.source(body)), css = "", structural = false) HTML_Document(title, content) } def preview_document( snapshot: Document.Snapshot, plain_text: Boolean = false, fonts_css: String = HTML.fonts_css() ): HTML_Document = { require(!snapshot.is_outdated, "document snapshot outdated") val name = snapshot.node_name if (plain_text) { val title = "File " + Symbol.cartouche_decoded(name.path.file_name) val body = HTML.text(snapshot.source) html_document(title, body, fonts_css) } else { Resources.html_document(snapshot) getOrElse { val title = if (name.is_theory) "Theory " + quote(name.theory_base_name) else "File " + Symbol.cartouche_decoded(name.path.file_name) val xml = snapshot.xml_markup(elements = elements.html) val body = Node_Context.empty.make_html(elements, xml) html_document(title, body, fonts_css) } } } /* maintain presentation structure */ def update_chapter(session_name: String, session_description: String): Unit = synchronized { val dir = Meta_Data.init_directory(chapter_dir(session_name)) Meta_Data.change(dir, Meta_Data.INDEX) { text => val index0 = Meta_Data.Index.parse(text, "chapter") val item = Meta_Data.Item(session_name, description = session_description) val index = index0 + item if (index != index0) { val title = "Isabelle/" + session_chapter(session_name) + " sessions" HTML.write_document(dir, "index.html", List(HTML.title(title + Isabelle_System.isabelle_heading())), HTML.chapter(title) :: (if (index.is_empty) Nil else List(HTML.div("sessions", List(HTML.description( index.items.map(item => (List(HTML.link(item.name + "/index.html", HTML.text(item.name))), if (item.description.isEmpty) Nil else HTML.break ::: List(HTML.pre(HTML.text(item.description)))))))))), root = Some(root_dir)) } index.print_json } } def update_root(): Unit = synchronized { Meta_Data.init_directory(root_dir) HTML.init_fonts(root_dir) Isabelle_System.copy_file(Path.explode("~~/lib/logo/isabelle.gif"), root_dir + Path.explode("isabelle.gif")) Meta_Data.change(root_dir, Meta_Data.INDEX) { text => val index0 = Meta_Data.Index.parse(text, "root") val index = { val items1 = sessions_structure.known_chapters .map(ch => Meta_Data.Item(ch.name, description = ch.description)) val items2 = index0.items.filterNot(item => items1.exists(_.name == item.name)) index0.copy(items = items1 ::: items2) } if (index != index0) { val title = "The " + XML.text(Isabelle_System.isabelle_name()) + " Library" HTML.write_document(root_dir, "index.html", List(HTML.title(title + Isabelle_System.isabelle_heading())), HTML.chapter(title) :: (if (index.is_empty) Nil else List(HTML.div("sessions", List(HTML.description( index.items.map(item => (List(HTML.link(item.name + "/index.html", HTML.text(item.name))), if (item.description.isEmpty) Nil else HTML.break ::: List(HTML.pre(HTML.text(item.description)))))))))), root = Some(root_dir)) } index.print_json } } } sealed case class HTML_Document(title: String, content: String) /* formal entities */ object Theory_Ref { def unapply(props: Properties.T): Option[String] = (props, props) match { case (Markup.Kind(Markup.THEORY), Markup.Name(theory)) => Some(theory) case _ => None } } object Entity_Ref { def unapply(props: Properties.T): Option[(String, String, String)] = (props, props, props, props) match { case (Markup.Entity.Ref.Prop(_), Position.Def_File(file), Markup.Kind(kind), Markup.Name(name)) if Path.is_wellformed(file) => Some((file, kind, name)) case _ => None } } object Node_Context { val empty: Node_Context = new Node_Context def make( context: Context, session_name: String, theory_name: String, file_name: String, node_dir: Path, ): Node_Context = new Node_Context { private val seen_ranges: mutable.Set[Symbol.Range] = mutable.Set.empty override def make_def(range: Symbol.Range, body: XML.Body): Option[XML.Elem] = body match { case List(XML.Elem(Markup("span", List("id" -> _)), _)) => None case _ => for (theory <- context.theory_by_name(session_name, theory_name)) yield { val body1 = if (seen_ranges.contains(range)) { HTML.entity_def(HTML.span(HTML.id(offset_id(range)), body)) } else HTML.span(body) theory.get_defs(file_name, range).foldLeft(body1) { case (elem, entity) => HTML.entity_def(HTML.span(HTML.id(entity.kname), List(elem))) } } } private def offset_id(range: Text.Range): String = "offset_" + range.start + ".." + range.stop override def make_file_ref(file: String, body: XML.Body): Option[XML.Elem] = { for (theory <- context.theory_by_file(session_name, file)) yield { val html_path = context.theory_dir(theory) + context.smart_html(theory, file) val html_link = HTML.relative_href(html_path, base = Some(node_dir)) HTML.link(html_link, body) } } override def make_ref(props: Properties.T, body: XML.Body): Option[XML.Elem] = { props match { case Theory_Ref(thy_name) => for (theory <- context.theory_by_name(session_name, thy_name)) yield { val html_path = context.theory_dir(theory) + context.theory_html(theory) val html_link = HTML.relative_href(html_path, base = Some(node_dir)) HTML.link(html_link, body) } case Entity_Ref(def_file, kind, name) => def logical_ref(theory: Document_Info.Theory): Option[String] = theory.get_def(def_file, kind, name).map(_.kname) def physical_ref(theory: Document_Info.Theory): Option[String] = props match { case Position.Def_Range(range) if theory.name == theory_name => seen_ranges += range Some(offset_id(range)) case _ => None } for { theory <- context.theory_by_file(session_name, def_file) html_ref <- logical_ref(theory) orElse physical_ref(theory) } yield { val html_path = context.theory_dir(theory) + context.smart_html(theory, def_file) val html_link = HTML.relative_href(html_path, base = Some(node_dir)) HTML.entity_ref(HTML.link(html_link + "#" + html_ref, body)) } case _ => None } } } } class Node_Context { def make_def(range: Symbol.Range, body: XML.Body): Option[XML.Elem] = None def make_ref(props: Properties.T, body: XML.Body): Option[XML.Elem] = None def make_file_ref(file: String, body: XML.Body): Option[XML.Elem] = None val div_elements: Set[String] = Set(HTML.div.name, HTML.pre.name, HTML.par.name, HTML.list.name, HTML.`enum`.name, HTML.descr.name) def make_html(elements: Elements, xml: XML.Body): XML.Body = { def html_div(html: XML.Body): Boolean = html exists { case XML.Elem(markup, body) => div_elements.contains(markup.name) || html_div(body) case XML.Text(_) => false } def html_class(c: String, html: XML.Body): XML.Body = if (c == "") html else if (html_div(html)) List(HTML.div(c, html)) else List(HTML.span(c, html)) def html_body(xml_body: XML.Body, end_offset: Symbol.Offset): (XML.Body, Symbol.Offset) = xml_body.foldRight((List.empty[XML.Tree], end_offset)) { case (tree, (res, end_offset1)) => val (res1, offset) = html_body_single(tree, end_offset1) (res1 ++ res, offset) } @tailrec def html_body_single(xml_tree: XML.Tree, end_offset: Symbol.Offset): (XML.Body, Symbol.Offset) = xml_tree match { case XML.Wrapped_Elem(markup, _, body) => html_body_single(XML.Elem(markup, body), end_offset) case XML.Elem(Markup(Markup.ENTITY, props @ Markup.Kind(kind)), body) => val (body1, offset) = html_body(body, end_offset) if (elements.entity(kind)) { make_ref(props, body1) match { case Some(link) => (List(link), offset) case None => (body1, offset) } } else (body1, offset) case XML.Elem(Markup.Path(file), body) => val (body1, offset) = html_body(body, end_offset) make_file_ref(file, body1) match { case Some(link) => (List(link), offset) case None => (body1, offset) } case XML.Elem(Markup.Url(href), body) => val (body1, offset) = html_body(body, end_offset) (List(HTML.link(href, body1)), offset) case XML.Elem(Markup(Markup.LANGUAGE, Markup.Name(name)), body) => val (body1, offset) = html_body(body, end_offset) (html_class(if (elements.language(name)) name else "", body1), offset) case XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), body) => val (body1, offset) = html_body(body, end_offset) (List(HTML.par(body1)), offset) case XML.Elem(Markup(Markup.MARKDOWN_ITEM, _), body) => val (body1, offset) = html_body(body, end_offset) (List(HTML.item(body1)), offset) case XML.Elem(Markup(Markup.Markdown_Bullet.name, _), text) => (Nil, end_offset - XML.symbol_length(text)) case XML.Elem(Markup.Markdown_List(kind), body) => val (body1, offset) = html_body(body, end_offset) if (kind == Markup.ENUMERATE) (List(HTML.`enum`(body1)), offset) else (List(HTML.list(body1)), offset) case XML.Elem(markup, body) => val name = markup.name val (body1, offset) = html_body(body, end_offset) val html = markup.properties match { case Markup.Kind(kind) if kind == Markup.COMMAND || kind == Markup.KEYWORD => html_class(kind, body1) case _ => body1 } Rendering.foreground.get(name) orElse Rendering.text_color.get(name) match { case Some(c) => (html_class(c.toString, html), offset) case None => (html_class(name, html), offset) } case XML.Text(text) => val offset = end_offset - Symbol.length(text) val body = HTML.text(Symbol.decode(text)) make_def(Text.Range(offset, end_offset), body) match { case Some(body1) => (List(body1), offset) case None => (body, offset) } } html_body(xml, XML.symbol_length(xml) + 1)._1 } } /** build presentation **/ val session_graph_path: Path = Path.explode("session_graph.pdf") def build_session( context: Context, session_context: Export.Session_Context, progress: Progress = new Progress, verbose: Boolean = false, ): Unit = { progress.expose_interrupt() val session_name = session_context.session_name val session_info = session_context.sessions_structure(session_name) val session_dir = context.session_dir(session_name).expand progress.echo("Presenting " + session_name + " in " + session_dir + " ...") Meta_Data.init_directory(context.chapter_dir(session_name)) Meta_Data.clean_directory(session_dir) val session = context.document_info.the_session(session_name) Bytes.write(session_dir + session_graph_path, graphview.Graph_File.make_pdf(session_info.options, session_context.session_base.session_graph_display)) val document_variants = for { doc <- session_info.document_variants db <- session_context.session_db() document <- Document_Build.read_document(db, session_name, doc.name) } yield { val doc_path = session_dir + doc.path.pdf if (Path.eq_case_insensitive(doc.path.pdf, session_graph_path)) { error("Illegal document variant " + quote(doc.name) + " (conflict with " + session_graph_path + ")") } if (verbose) progress.echo("Presenting document " + session_name + "/" + doc.name) if (session_info.document_echo) progress.echo("Document at " + doc_path) Bytes.write(doc_path, document.pdf) doc } val document_links = { val link1 = HTML.link(session_graph_path, HTML.text("theory dependencies")) val links2 = document_variants.map(doc => HTML.link(doc.path.pdf, HTML.text(doc.name))) Library.separate(HTML.break ::: HTML.nl, (link1 :: links2).map(link => HTML.text("View ") ::: List(link))).flatten } def present_theory(theory_name: String): XML.Body = { progress.expose_interrupt() def err(): Nothing = error("Missing document information for theory: " + quote(theory_name)) - val command = Build_Job.read_theory(session_context.theory(theory_name)) getOrElse err() + val snapshot = Build_Job.read_theory(session_context.theory(theory_name)) getOrElse err() val theory = context.theory_by_name(session_name, theory_name) getOrElse err() if (verbose) progress.echo("Presenting theory " + quote(theory_name)) - val snapshot = Document.State.init.snippet(command) val thy_elements = theory.elements(context.elements) def node_context(file_name: String, node_dir: Path): Node_Context = Node_Context.make(context, session_name, theory_name, file_name, node_dir) val thy_html = context.source( node_context(theory.thy_file, session_dir). make_html(thy_elements, snapshot.xml_markup(elements = thy_elements.html))) val files = for { (blob, xml) <- snapshot.xml_markup_blobs(elements = thy_elements.html) if xml.nonEmpty } yield { progress.expose_interrupt() val file_name = blob.name.node if (verbose) progress.echo("Presenting file " + quote(file_name)) val file_html = session_dir + context.file_html(file_name) val file_dir = file_html.dir val html_link = HTML.relative_href(file_html, base = Some(session_dir)) val html = context.source(node_context(file_name, file_dir).make_html(thy_elements, xml)) val file_title = "File " + Symbol.cartouche_decoded(blob.src_path.implode_short) HTML.write_document(file_dir, file_html.file_name, List(HTML.title(file_title)), List(context.head(file_title), html), root = Some(context.root_dir)) List(HTML.link(html_link, HTML.text(file_title))) } val thy_title = "Theory " + theory.print_short HTML.write_document(session_dir, context.theory_html(theory).implode, List(HTML.title(thy_title)), List(context.head(thy_title), thy_html), root = Some(context.root_dir)) List(HTML.link(context.theory_html(theory), HTML.text(theory.print_short) ::: (if (files.isEmpty) Nil else List(HTML.itemize(files))))) } val theories = session.used_theories.map(present_theory) val title = "Session " + session_name HTML.write_document(session_dir, "index.html", List(HTML.title(title + Isabelle_System.isabelle_heading())), context.head(title, List(HTML.par(document_links))) :: context.contents("Theories", theories), root = Some(context.root_dir)) Meta_Data.set_build_uuid(session_dir, session.build_uuid) context.update_chapter(session_name, session_info.description) } def build( browser_info: Config, store: Sessions.Store, deps: Sessions.Deps, sessions: List[String], progress: Progress = new Progress, verbose: Boolean = false ): Unit = { val root_dir = browser_info.presentation_dir(store).absolute progress.echo("Presentation in " + root_dir) using(Export.open_database_context(store)) { database_context => val context0 = context(deps.sessions_structure, root_dir = root_dir) val sessions1 = deps.sessions_structure.build_requirements(sessions).filter { session_name => using(database_context.open_database(session_name)) { session_database => database_context.store.read_build(session_database.db, session_name) match { case None => false case Some(build) => val session_dir = context0.session_dir(session_name) !Meta_Data.check_build_uuid(session_dir, build.uuid) } } } val context1 = context(deps.sessions_structure, root_dir = root_dir, document_info = Document_Info.read(database_context, deps, sessions1)) context1.update_root() Par_List.map({ (session: String) => using(database_context.open_session(deps.base_info(session))) { session_context => build_session(context1, session_context, progress = progress, verbose = verbose) } }, sessions1) } } } 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,580 +1,582 @@ /* 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[Command] = { + ): 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)) - Command.unparsed(thy_source, theory = true, id = id, node_name = node_name, - blobs_info = blobs_info, results = results, markups = markups) + 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.empty) 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(command) => - val snapshot = Document.State.init.snippet(command) + 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(command.source) + 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, command.node_name.node) + 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_name: String, val info: Sessions.Info, deps: Sessions.Deps, store: Sessions.Store, do_store: Boolean, log: Logger, session_setup: (String, Session) => Unit, val numa_node: Option[Int], command_timings0: List[Properties.T] ) { val options: Options = NUMA.policy_options(info.options, numa_node) private val sessions_structure = deps.sessions_structure private val future_result: Future[Process_Result] = Future.thread("build", uninterruptible = true) { val parent = info.parent.getOrElse("") val base = deps(parent) val result_base = deps(session_name) 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(sessions_structure, base, 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 = { result_base.load_commands.get(name.expand) match { case Some(spans) => val syntax = result_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(session, options, sessions_structure, store, 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(deps.base_info(session_name))) { 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.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, _) <- deps(session_name).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/Pure/Tools/profiling_report.scala b/src/Pure/Tools/profiling_report.scala --- a/src/Pure/Tools/profiling_report.scala +++ b/src/Pure/Tools/profiling_report.scala @@ -1,80 +1,79 @@ /* Title: Pure/Tools/profiling_report.scala Author: Makarius Report Poly/ML profiling information from session build database. */ package isabelle object Profiling_Report { def profiling_report( options: Options, session: String, theories: List[String] = Nil, clean_name: Boolean = false, progress: Progress = new Progress ): Unit = { val store = Sessions.store(options) using(Export.open_session_context0(store, session)) { session_context => session_context.session_db().map(db => store.read_theories(db, session)) match { case None => store.error_database(session) case Some(used_theories) => theories.filterNot(used_theories.toSet) match { case Nil => case bad => error("Unknown theories " + commas_quote(bad)) } val reports = (for { thy <- used_theories.iterator if theories.isEmpty || theories.contains(thy) - command <- Build_Job.read_theory(session_context.theory(thy)).iterator - snapshot = Document.State.init.snippet(command) + snapshot <- Build_Job.read_theory(session_context.theory(thy)).iterator (Protocol.ML_Profiling(report), _) <- snapshot.messages.iterator } yield if (clean_name) report.clean_name else report).toList for (report <- ML_Profiling.account(reports)) progress.echo(report.print) } } } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("profiling_report", "report Poly/ML profiling information from log files", Scala_Project.here, { args => var theories: List[String] = Nil var clean_name = false var options = Options.init() val getopts = Getopts(""" Usage: isabelle profiling_report [OPTIONS] SESSION Options are: -T NAME restrict to given theories (multiple options possible) -c clean function names -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) Report Poly/ML profiling from the build database of the given session (without up-to-date check of sources). """, "T:" -> (arg => theories = theories ::: List(arg)), "c" -> (_ => clean_name = true), "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() profiling_report(options, session_name, theories = theories, clean_name = clean_name, progress = progress) }) }