diff --git a/src/Pure/PIDE/xml.scala b/src/Pure/PIDE/xml.scala --- a/src/Pure/PIDE/xml.scala +++ b/src/Pure/PIDE/xml.scala @@ -1,428 +1,429 @@ /* Title: Pure/PIDE/xml.scala Author: Makarius Untyped XML trees and basic data representation. */ package isabelle object XML { /** XML trees **/ /* datatype representation */ type Attribute = Properties.Entry type Attributes = Properties.T sealed abstract class Tree { override def toString: String = string_of_tree(this) } type Body = List[Tree] case class Elem(markup: Markup, body: Body) extends Tree { def name: String = markup.name def update_attributes(more_attributes: Attributes): Elem = if (more_attributes.isEmpty) this else Elem(markup.update_properties(more_attributes), body) def + (att: Attribute): Elem = Elem(markup + att, body) } case class Text(content: String) extends Tree def elem(markup: Markup): XML.Elem = XML.Elem(markup, Nil) def elem(name: String, body: Body): XML.Elem = XML.Elem(Markup(name, Nil), body) def elem(name: String): XML.Elem = XML.Elem(Markup(name, Nil), Nil) + val no_text: Text = Text("") val newline: Text = Text("\n") /* name space */ object Namespace { def apply(prefix: String, target: String): Namespace = new Namespace(prefix, target) } final class Namespace private(prefix: String, target: String) { def apply(name: String): String = prefix + ":" + name val attribute: XML.Attribute = ("xmlns:" + prefix, target) override def toString: String = attribute.toString } /* wrapped elements */ val XML_ELEM = "xml_elem" val XML_NAME = "xml_name" val XML_BODY = "xml_body" object Wrapped_Elem { def apply(markup: Markup, body1: Body, body2: Body): XML.Elem = XML.Elem(Markup(XML_ELEM, (XML_NAME, markup.name) :: markup.properties), XML.Elem(Markup(XML_BODY, Nil), body1) :: body2) def unapply(tree: Tree): Option[(Markup, Body, Body)] = tree match { case XML.Elem(Markup(XML_ELEM, (XML_NAME, name) :: props), XML.Elem(Markup(XML_BODY, Nil), body1) :: body2) => Some(Markup(name, props), body1, body2) case _ => None } } object Root_Elem { def apply(body: Body): XML.Elem = XML.Elem(Markup(XML_ELEM, Nil), body) def unapply(tree: Tree): Option[Body] = tree match { case XML.Elem(Markup(XML_ELEM, Nil), body) => Some(body) case _ => None } } /* traverse text */ def traverse_text[A](body: Body)(a: A)(op: (A, String) => A): A = { def traverse(x: A, t: Tree): A = t match { case XML.Wrapped_Elem(_, _, ts) => (x /: ts)(traverse) case XML.Elem(_, ts) => (x /: ts)(traverse) case XML.Text(s) => op(x, s) } (a /: body)(traverse) } def text_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + s.length } /* text content */ def content(body: Body): String = { val text = new StringBuilder(text_length(body)) traverse_text(body)(()) { case (_, s) => text.append(s) } text.toString } def content(tree: Tree): String = content(List(tree)) /** string representation **/ val header: String = "\n" def output_char(c: Char, s: StringBuilder) { c match { case '<' => s ++= "<" case '>' => s ++= ">" case '&' => s ++= "&" case '"' => s ++= """ case '\'' => s ++= "'" case _ => s += c } } def output_string(str: String, s: StringBuilder) { if (str == null) s ++= str else str.iterator.foreach(c => output_char(c, s)) } def string_of_body(body: Body): String = { val s = new StringBuilder def text(txt: String) { output_string(txt, s) } def elem(markup: Markup) { s ++= markup.name for ((a, b) <- markup.properties) { s += ' '; s ++= a; s += '='; s += '"'; text(b); s += '"' } } def tree(t: Tree): Unit = t match { case XML.Elem(markup, Nil) => s += '<'; elem(markup); s ++= "/>" case XML.Elem(markup, ts) => s += '<'; elem(markup); s += '>' ts.foreach(tree) s ++= "' case XML.Text(txt) => text(txt) } body.foreach(tree) s.toString } def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree)) /** cache **/ object Cache { def make( max_string: Int = isabelle.Cache.default_max_string, initial_size: Int = isabelle.Cache.default_initial_size): Cache = new Cache(max_string, initial_size) val none: Cache = make(max_string = 0) } class Cache private[XML](max_string: Int, initial_size: Int) extends isabelle.Cache(max_string, initial_size) { protected def cache_props(x: Properties.T): Properties.T = { if (x.isEmpty) x else lookup(x) match { case Some(y) => y case None => store(x.map(p => (Library.isolate_substring(p._1).intern, cache_string(p._2)))) } } protected def cache_markup(x: Markup): Markup = { lookup(x) match { case Some(y) => y case None => x match { case Markup(name, props) => store(Markup(cache_string(name), cache_props(props))) } } } protected def cache_tree(x: XML.Tree): XML.Tree = { lookup(x) match { case Some(y) => y case None => x match { case XML.Elem(markup, body) => store(XML.Elem(cache_markup(markup), cache_body(body))) case XML.Text(text) => store(XML.Text(cache_string(text))) } } } protected def cache_body(x: XML.Body): XML.Body = { if (x.isEmpty) x else lookup(x) match { case Some(y) => y case None => x.map(cache_tree) } } // main methods def props(x: Properties.T): Properties.T = if (no_cache) x else synchronized { cache_props(x) } def markup(x: Markup): Markup = if (no_cache) x else synchronized { cache_markup(x) } def tree(x: XML.Tree): XML.Tree = if (no_cache) x else synchronized { cache_tree(x) } def body(x: XML.Body): XML.Body = if (no_cache) x else synchronized { cache_body(x) } def elem(x: XML.Elem): XML.Elem = if (no_cache) x else synchronized { cache_tree(x).asInstanceOf[XML.Elem] } } /** XML as data representation language **/ abstract class Error(s: String) extends Exception(s) class XML_Atom(s: String) extends Error(s) class XML_Body(body: XML.Body) extends Error("") object Encode { type T[A] = A => XML.Body type V[A] = PartialFunction[A, (List[String], XML.Body)] type P[A] = PartialFunction[A, List[String]] /* atomic values */ def long_atom(i: Long): String = Library.signed_string_of_long(i) def int_atom(i: Int): String = Library.signed_string_of_int(i) def bool_atom(b: Boolean): String = if (b) "1" else "0" def unit_atom(u: Unit) = "" /* structural nodes */ private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts) private def vector(xs: List[String]): XML.Attributes = xs.zipWithIndex.map({ case (x, i) => (int_atom(i), x) }) private def tagged(tag: Int, data: (List[String], XML.Body)): XML.Tree = XML.Elem(Markup(int_atom(tag), vector(data._1)), data._2) /* representation of standard types */ val tree: T[XML.Tree] = (t => List(t)) val properties: T[Properties.T] = (props => List(XML.Elem(Markup(":", props), Nil))) val string: T[String] = (s => if (s.isEmpty) Nil else List(XML.Text(s))) val long: T[Long] = (x => string(long_atom(x))) val int: T[Int] = (x => string(int_atom(x))) val bool: T[Boolean] = (x => string(bool_atom(x))) val unit: T[Unit] = (x => string(unit_atom(x))) def pair[A, B](f: T[A], g: T[B]): T[(A, B)] = (x => List(node(f(x._1)), node(g(x._2)))) def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] = (x => List(node(f(x._1)), node(g(x._2)), node(h(x._3)))) def list[A](f: T[A]): T[List[A]] = (xs => xs.map((x: A) => node(f(x)))) def option[A](f: T[A]): T[Option[A]] = { case None => Nil case Some(x) => List(node(f(x))) } def variant[A](fs: List[V[A]]): T[A] = { case x => val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get List(tagged(tag, f(x))) } } object Decode { type T[A] = XML.Body => A type V[A] = (List[String], XML.Body) => A type P[A] = PartialFunction[List[String], A] /* atomic values */ def long_atom(s: String): Long = try { java.lang.Long.parseLong(s) } catch { case e: NumberFormatException => throw new XML_Atom(s) } def int_atom(s: String): Int = try { Integer.parseInt(s) } catch { case e: NumberFormatException => throw new XML_Atom(s) } def bool_atom(s: String): Boolean = if (s == "1") true else if (s == "0") false else throw new XML_Atom(s) def unit_atom(s: String): Unit = if (s == "") () else throw new XML_Atom(s) /* structural nodes */ private def node(t: XML.Tree): XML.Body = t match { case XML.Elem(Markup(":", Nil), ts) => ts case _ => throw new XML_Body(List(t)) } private def vector(atts: XML.Attributes): List[String] = atts.iterator.zipWithIndex.map( { case ((a, x), i) => if (int_atom(a) == i) x else throw new XML_Atom(a) }).toList private def tagged(t: XML.Tree): (Int, (List[String], XML.Body)) = t match { case XML.Elem(Markup(name, atts), ts) => (int_atom(name), (vector(atts), ts)) case _ => throw new XML_Body(List(t)) } /* representation of standard types */ val tree: T[XML.Tree] = { case List(t) => t case ts => throw new XML_Body(ts) } val properties: T[Properties.T] = { case List(XML.Elem(Markup(":", props), Nil)) => props case ts => throw new XML_Body(ts) } val string: T[String] = { case Nil => "" case List(XML.Text(s)) => s case ts => throw new XML_Body(ts) } val long: T[Long] = (x => long_atom(string(x))) val int: T[Int] = (x => int_atom(string(x))) val bool: T[Boolean] = (x => bool_atom(string(x))) val unit: T[Unit] = (x => unit_atom(string(x))) def pair[A, B](f: T[A], g: T[B]): T[(A, B)] = { case List(t1, t2) => (f(node(t1)), g(node(t2))) case ts => throw new XML_Body(ts) } def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] = { case List(t1, t2, t3) => (f(node(t1)), g(node(t2)), h(node(t3))) case ts => throw new XML_Body(ts) } def list[A](f: T[A]): T[List[A]] = (ts => ts.map(t => f(node(t)))) def option[A](f: T[A]): T[Option[A]] = { case Nil => None case List(t) => Some(f(node(t))) case ts => throw new XML_Body(ts) } def variant[A](fs: List[V[A]]): T[A] = { case List(t) => val (tag, (xs, ts)) = tagged(t) val f = try { fs(tag) } catch { case _: IndexOutOfBoundsException => throw new XML_Body(List(t)) } f(xs, ts) case ts => throw new XML_Body(ts) } } } diff --git a/src/Pure/PIDE/yxml.scala b/src/Pure/PIDE/yxml.scala --- a/src/Pure/PIDE/yxml.scala +++ b/src/Pure/PIDE/yxml.scala @@ -1,155 +1,155 @@ /* Title: Pure/PIDE/yxml.scala Author: Makarius Efficient text representation of XML trees. Suitable for direct inlining into plain text. */ package isabelle import scala.collection.mutable object YXML { /* chunk markers */ val X = '\u0005' val Y = '\u0006' val is_X = (c: Char) => c == X val is_Y = (c: Char) => c == Y val X_string: String = X.toString val Y_string: String = Y.toString val XY_string: String = X_string + Y_string val XYX_string: String = XY_string + X_string def detect(s: String): Boolean = s.exists(c => c == X || c == Y) def detect_elem(s: String): Boolean = s.startsWith(XY_string) /* string representation */ // FIXME byte array version with pseudo-utf-8 (!?) def traversal(string: String => Unit, body: XML.Body): Unit = { def tree(t: XML.Tree): Unit = t match { case XML.Elem(Markup(name, atts), ts) => string(XY_string) string(name) for ((a, x) <- atts) { string(Y_string); string(a); string("="); string(x) } string(X_string) ts.foreach(tree) string(XYX_string) case XML.Text(text) => string(text) } body.foreach(tree) } def string_of_body(body: XML.Body): String = { val s = new StringBuilder traversal(str => s ++= str, body) s.toString } def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree)) /* parsing */ private def err(msg: String) = error("Malformed YXML: " + msg) private def err_attribute() = err("bad attribute") private def err_element() = err("bad element") private def err_unbalanced(name: String) = if (name == "") err("unbalanced element") else err("unbalanced element " + quote(name)) private def parse_attrib(source: CharSequence) = { val s = source.toString val i = s.indexOf('=') if (i <= 0) err_attribute() (s.substring(0, i), s.substring(i + 1)) } def parse_body(source: CharSequence): XML.Body = { /* stack operations */ def buffer(): mutable.ListBuffer[XML.Tree] = new mutable.ListBuffer[XML.Tree] var stack: List[(Markup, mutable.ListBuffer[XML.Tree])] = List((Markup.Empty, buffer())) def add(x: XML.Tree) { (stack: @unchecked) match { case ((_, body) :: _) => body += x } } def push(name: String, atts: XML.Attributes) { if (name == "") err_element() else stack = (Markup(name, atts), buffer()) :: stack } def pop() { (stack: @unchecked) match { case ((Markup.Empty, _) :: _) => err_unbalanced("") case ((markup, body) :: pending) => stack = pending add(XML.Elem(markup, body.toList)) } } /* parse chunks */ for (chunk <- Library.separated_chunks(is_X, source) if chunk.length != 0) { if (chunk.length == 1 && chunk.charAt(0) == Y) pop() else { Library.separated_chunks(is_Y, chunk).toList match { case ch :: name :: atts if ch.length == 0 => push(name.toString, atts.map(parse_attrib)) case txts => for (txt <- txts) add(XML.Text(txt.toString)) } } } (stack: @unchecked) match { case List((Markup.Empty, body)) => body.toList case (Markup(name, _), _) :: _ => err_unbalanced(name) } } def parse(source: CharSequence): XML.Tree = parse_body(source) match { case List(result) => result - case Nil => XML.Text("") + case Nil => XML.no_text case _ => err("multiple XML trees") } def parse_elem(source: CharSequence): XML.Tree = parse_body(source) match { case List(elem: XML.Elem) => elem case _ => err("single XML element expected") } /* failsafe parsing */ private def markup_broken(source: CharSequence) = XML.Elem(Markup.Broken, List(XML.Text(source.toString))) def parse_body_failsafe(source: CharSequence): XML.Body = { try { parse_body(source) } catch { case ERROR(_) => List(markup_broken(source)) } } def parse_failsafe(source: CharSequence): XML.Tree = { try { parse(source) } catch { case ERROR(_) => markup_broken(source) } } } diff --git a/src/Pure/Thy/html.scala b/src/Pure/Thy/html.scala --- a/src/Pure/Thy/html.scala +++ b/src/Pure/Thy/html.scala @@ -1,401 +1,400 @@ /* Title: Pure/Thy/html.scala Author: Makarius HTML presentation elements. */ package isabelle object HTML { /* output text with control symbols */ private val control = Map( Symbol.sub -> "sub", Symbol.sub_decoded -> "sub", Symbol.sup -> "sup", Symbol.sup_decoded -> "sup", Symbol.bold -> "b", Symbol.bold_decoded -> "b") private val control_block = Map( Symbol.bsub -> "", Symbol.bsub_decoded -> "", Symbol.esub -> "", Symbol.esub_decoded -> "", Symbol.bsup -> "", Symbol.bsup_decoded -> "", Symbol.esup -> "", Symbol.esup_decoded -> "") def is_control(sym: Symbol.Symbol): Boolean = control.isDefinedAt(sym) def output_char_permissive(c: Char, s: StringBuilder) { c match { case '<' => s ++= "<" case '>' => s ++= ">" case '&' => s ++= "&" case _ => s += c } } def output(text: String, s: StringBuilder, hidden: Boolean, permissive: Boolean) { def output_char(c: Char): Unit = if (permissive) output_char_permissive(c, s) else XML.output_char(c, s) def output_string(str: String): Unit = str.iterator.foreach(output_char) def output_hidden(body: => Unit): Unit = if (hidden) { s ++= ""; body; s ++= "" } def output_symbol(sym: Symbol.Symbol): Unit = if (sym != "") { control_block.get(sym) match { case Some(html) if html.startsWith(" s ++= html; output_hidden(output_string(sym)) case Some(html) => output_hidden(output_string(sym)); s ++= html case None => if (hidden && Symbol.is_control_encoded(sym)) { output_hidden(output_string(Symbol.control_prefix)) s ++= "" output_string(Symbol.control_name(sym).get) s ++= "" output_hidden(output_string(Symbol.control_suffix)) } else output_string(sym) } } var ctrl = "" for (sym <- Symbol.iterator(text)) { if (is_control(sym)) { output_symbol(ctrl); ctrl = sym } else { control.get(ctrl) match { case Some(elem) if Symbol.is_controllable(sym) => output_hidden(output_symbol(ctrl)) s += '<'; s ++= elem; s += '>' output_symbol(sym) s ++= "' case _ => output_symbol(ctrl) output_symbol(sym) } ctrl = "" } } output_symbol(ctrl) } def output(text: String): String = Library.make_string(output(text, _, hidden = false, permissive = true)) /* output XML as HTML */ private val structural_elements = Set("head", "body", "meta", "div", "pre", "p", "title", "h1", "h2", "h3", "h4", "h5", "h6", "ul", "ol", "dl", "li", "dt", "dd") def output(body: XML.Body, s: StringBuilder, hidden: Boolean, structural: Boolean) { def elem(markup: Markup) { s ++= markup.name for ((a, b) <- markup.properties) { s += ' ' s ++= a s += '=' s += '"' output(b, s, hidden = hidden, permissive = false) s += '"' } } def tree(t: XML.Tree): Unit = t match { case XML.Elem(markup, Nil) => s += '<'; elem(markup); s ++= "/>" case XML.Elem(markup, ts) => if (structural && structural_elements(markup.name)) s += '\n' s += '<'; elem(markup); s += '>' ts.foreach(tree) s ++= "' if (structural && structural_elements(markup.name)) s += '\n' case XML.Text(txt) => output(txt, s, hidden = hidden, permissive = true) } body.foreach(tree) } def output(body: XML.Body, hidden: Boolean, structural: Boolean): String = Library.make_string(output(body, _, hidden, structural)) def output(tree: XML.Tree, hidden: Boolean, structural: Boolean): String = output(List(tree), hidden, structural) /* attributes */ class Attribute(val name: String, value: String) { def xml: XML.Attribute = name -> value def apply(elem: XML.Elem): XML.Elem = elem + xml } def id(s: String): Attribute = new Attribute("id", s) def class_(name: String): Attribute = new Attribute("class", name) def width(w: Int): Attribute = new Attribute("width", w.toString) def height(h: Int): Attribute = new Attribute("height", h.toString) def size(w: Int, h: Int)(elem: XML.Elem): XML.Elem = width(w)(height(h)(elem)) /* structured markup operators */ def text(txt: String): XML.Body = if (txt.isEmpty) Nil else List(XML.Text(txt)) - val no_text: XML.Tree = XML.Text("") val break: XML.Body = List(XML.elem("br")) val nl: XML.Body = List(XML.Text("\n")) class Operator(val name: String) { def apply(body: XML.Body): XML.Elem = XML.elem(name, body) def apply(att: Attribute, body: XML.Body): XML.Elem = att(apply(body)) def apply(c: String, body: XML.Body): XML.Elem = apply(class_(c), body) } class Heading(name: String) extends Operator(name) { def apply(txt: String): XML.Elem = super.apply(text(txt)) def apply(att: Attribute, txt: String): XML.Elem = super.apply(att, text(txt)) def apply(c: String, txt: String): XML.Elem = super.apply(c, text(txt)) } val div = new Operator("div") val span = new Operator("span") val pre = new Operator("pre") val par = new Operator("p") val emph = new Operator("em") val bold = new Operator("b") val code = new Operator("code") val item = new Operator("li") val list = new Operator("ul") val enum = new Operator("ol") val descr = new Operator("dl") val dt = new Operator("dt") val dd = new Operator("dd") val title = new Heading("title") val chapter = new Heading("h1") val section = new Heading("h2") val subsection = new Heading("h3") val subsubsection = new Heading("h4") val paragraph = new Heading("h5") val subparagraph = new Heading("h6") def itemize(items: List[XML.Body]): XML.Elem = list(items.map(item(_))) def enumerate(items: List[XML.Body]): XML.Elem = enum(items.map(item(_))) def description(items: List[(XML.Body, XML.Body)]): XML.Elem = descr(items.flatMap({ case (x, y) => List(dt(x), dd(y)) })) def link(href: String, body: XML.Body): XML.Elem = XML.Elem(Markup("a", List("href" -> href)), if (body.isEmpty) text(href) else body) def link(path: Path, body: XML.Body): XML.Elem = link(path.implode, body) def image(src: String, alt: String = ""): XML.Elem = XML.Elem(Markup("img", List("src" -> src) ::: proper_string(alt).map("alt" -> _).toList), Nil) def source(body: XML.Body): XML.Elem = pre("source", body) def source(src: String): XML.Elem = source(text(src)) def style(s: String): XML.Elem = XML.elem("style", text(s)) def style_file(href: String): XML.Elem = XML.Elem(Markup("link", List("rel" -> "stylesheet", "type" -> "text/css", "href" -> href)), Nil) def style_file(path: Path): XML.Elem = style_file(Url.print_file(path.file)) def script(s: String): XML.Elem = XML.elem("script", text(s)) def script_file(href: String): XML.Elem = XML.Elem(Markup("script", List("src" -> href)), Nil) def script_file(path: Path): XML.Elem = script_file(Url.print_file(path.file)) /* messages */ // background val writeln_message: Attribute = class_("writeln_message") val warning_message: Attribute = class_("warning_message") val error_message: Attribute = class_("error_message") // underline val writeln: Attribute = class_("writeln") val warning: Attribute = class_("warning") val error: Attribute = class_("error") /* tooltips */ def tooltip(item: XML.Body, tip: XML.Body): XML.Elem = span(item ::: List(div("tooltip", tip))) def tooltip_errors(item: XML.Body, msgs: List[XML.Body]): XML.Elem = HTML.error(tooltip(item, msgs.map(msg => error_message(pre(msg))))) /* GUI elements */ object GUI { private def optional_value(text: String): XML.Attributes = proper_string(text).map(a => "value" -> a).toList private def optional_name(name: String): XML.Attributes = proper_string(name).map(a => "name" -> a).toList private def optional_title(tooltip: String): XML.Attributes = proper_string(tooltip).map(a => "title" -> a).toList private def optional_submit(submit: Boolean): XML.Attributes = if (submit) List("onChange" -> "this.form.submit()") else Nil private def optional_checked(selected: Boolean): XML.Attributes = if (selected) List("checked" -> "") else Nil private def optional_action(action: String): XML.Attributes = proper_string(action).map(a => "action" -> a).toList private def optional_onclick(script: String): XML.Attributes = proper_string(script).map(a => "onclick" -> a).toList private def optional_onchange(script: String): XML.Attributes = proper_string(script).map(a => "onchange" -> a).toList def button(body: XML.Body, name: String = "", tooltip: String = "", submit: Boolean = false, script: String = ""): XML.Elem = XML.Elem( Markup("button", List("type" -> (if (submit) "submit" else "button"), "value" -> "true") ::: optional_name(name) ::: optional_title(tooltip) ::: optional_onclick(script)), body) def checkbox(body: XML.Body, name: String = "", tooltip: String = "", submit: Boolean = false, selected: Boolean = false, script: String = ""): XML.Elem = XML.elem("label", XML.elem( Markup("input", List("type" -> "checkbox", "value" -> "true") ::: optional_name(name) ::: optional_title(tooltip) ::: optional_submit(submit) ::: optional_checked(selected) ::: optional_onchange(script))) :: body) def text_field(columns: Int = 0, text: String = "", name: String = "", tooltip: String = "", submit: Boolean = false, script: String = ""): XML.Elem = XML.elem(Markup("input", List("type" -> "text") ::: (if (columns > 0) List("size" -> columns.toString) else Nil) ::: optional_value(text) ::: optional_name(name) ::: optional_title(tooltip) ::: optional_submit(submit) ::: optional_onchange(script))) def parameter(text: String = "", name: String = ""): XML.Elem = XML.elem( Markup("input", List("type" -> "hidden") ::: optional_value(text) ::: optional_name(name))) def form(body: XML.Body, name: String = "", action: String = "", http_post: Boolean = false) : XML.Elem = XML.Elem( Markup("form", optional_name(name) ::: optional_action(action) ::: (if (http_post) List("method" -> "post") else Nil)), body) } /* GUI layout */ object Wrap_Panel { object Alignment extends Enumeration { val left, right, center = Value } def apply(contents: List[XML.Elem], name: String = "", action: String = "", alignment: Alignment.Value = Alignment.right): XML.Elem = { val body = Library.separate(XML.Text(" "), contents) GUI.form(List(div(body) + ("style" -> ("text-align: " + alignment))), name = name, action = action) } } /* document */ val header: String = XML.header + """ """ val head_meta: XML.Elem = XML.Elem(Markup("meta", List("http-equiv" -> "Content-Type", "content" -> "text/html; charset=utf-8")), Nil) def output_document(head: XML.Body, body: XML.Body, css: String = "isabelle.css", hidden: Boolean = true, structural: Boolean = true): String = { cat_lines( List(header, output( XML.elem("head", head_meta :: (if (css == "") Nil else List(style_file(css))) ::: head), hidden = hidden, structural = structural), output(XML.elem("body", body), hidden = hidden, structural = structural))) } /* fonts */ def fonts_url(): String => String = (for (entry <- Isabelle_Fonts.fonts(hidden = true)) yield (entry.path.file_name -> Url.print_file(entry.path.file))).toMap def fonts_dir(prefix: String)(ttf_name: String): String = prefix + "/" + ttf_name def fonts_css(make_url: String => String = fonts_url()): String = { def font_face(entry: Isabelle_Fonts.Entry): String = cat_lines( List( "@font-face {", " font-family: '" + entry.family + "';", " src: url('" + make_url(entry.path.file_name) + "') format('truetype');") ::: (if (entry.is_bold) List(" font-weight: bold;") else Nil) ::: (if (entry.is_italic) List(" font-style: italic;") else Nil) ::: List("}")) ("/* Isabelle fonts */" :: Isabelle_Fonts.fonts(hidden = true).map(font_face)) .mkString("", "\n\n", "\n") } /* document directory */ def isabelle_css: Path = Path.explode("~~/etc/isabelle.css") def write_isabelle_css(dir: Path, make_url: String => String = fonts_dir("fonts")) { File.write(dir + isabelle_css.base, fonts_css(make_url) + "\n\n" + File.read(isabelle_css)) } def init_dir(dir: Path): Unit = write_isabelle_css(Isabelle_System.make_directory(dir)) def write_document(dir: Path, name: String, head: XML.Body, body: XML.Body, css: String = isabelle_css.file_name, hidden: Boolean = true, structural: Boolean = true) { init_dir(dir) File.write(dir + Path.basic(name), output_document(head, body, css = css, hidden = hidden, structural = structural)) } } diff --git a/src/Pure/Thy/presentation.scala b/src/Pure/Thy/presentation.scala --- a/src/Pure/Thy/presentation.scala +++ b/src/Pure/Thy/presentation.scala @@ -1,770 +1,770 @@ /* Title: Pure/Thy/present.scala Author: Makarius HTML/PDF presentation of theory documents. */ package isabelle import scala.collection.immutable.SortedMap object Presentation { /** HTML documents **/ val fonts_path = Path.explode("fonts") sealed case class HTML_Document(title: String, content: String) def html_context(fonts_url: String => String = HTML.fonts_url()): HTML_Context = new HTML_Context(fonts_url) final class HTML_Context private[Presentation](fonts_url: String => String) { def init_fonts(dir: Path) { val fonts_dir = Isabelle_System.make_directory(dir + fonts_path) for (entry <- Isabelle_Fonts.fonts(hidden = true)) File.copy(entry.path, fonts_dir) } 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)))) } def output_document(title: String, body: XML.Body): String = HTML.output_document( List( HTML.style(HTML.fonts_css(fonts_url) + "\n\n" + File.read(HTML.isabelle_css)), HTML.title(title)), List(HTML.source(body)), css = "", structural = false) def html_document(title: String, body: XML.Body): HTML_Document = HTML_Document(title, output_document(title, body)) } /* HTML body */ private val div_elements = Set(HTML.div.name, HTML.pre.name, HTML.par.name, HTML.list.name, HTML.enum.name, HTML.descr.name) private 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 } private def html_class(c: String, html: XML.Body): XML.Tree = - if (html.forall(_ == HTML.no_text)) HTML.no_text + if (html.forall(_ == XML.no_text)) XML.no_text else if (html_div(html)) HTML.div(c, html) else HTML.span(c, html) private def html_body(xml: XML.Body): XML.Body = xml map { case XML.Elem(Markup(Markup.LANGUAGE, Markup.Name(Markup.Language.DOCUMENT)), body) => html_class(Markup.Language.DOCUMENT, html_body(body)) case XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), body) => HTML.par(html_body(body)) case XML.Elem(Markup(Markup.MARKDOWN_ITEM, _), body) => HTML.item(html_body(body)) - case XML.Elem(Markup(Markup.Markdown_Bullet.name, _), _) => HTML.no_text + case XML.Elem(Markup(Markup.Markdown_Bullet.name, _), _) => XML.no_text case XML.Elem(Markup.Markdown_List(kind), body) => if (kind == Markup.ENUMERATE) HTML.enum(html_body(body)) else HTML.list(html_body(body)) case XML.Elem(markup, body) => val name = markup.name val html = markup.properties match { case Markup.Kind(kind) if kind == Markup.COMMAND || kind == Markup.KEYWORD => List(html_class(kind, html_body(body))) case _ => html_body(body) } Rendering.foreground.get(name) orElse Rendering.text_color.get(name) match { case Some(c) => html_class(c.toString, html) case None => html_class(name, html) } case XML.Text(text) => XML.Text(Symbol.decode(text)) } /* PIDE HTML document */ val html_elements: Markup.Elements = Rendering.foreground_elements ++ Rendering.text_color_elements ++ Rendering.markdown_elements + Markup.NUMERAL + Markup.COMMENT + Markup.LANGUAGE def html_document( resources: Resources, snapshot: Document.Snapshot, html_context: HTML_Context, plain_text: Boolean = false): HTML_Document = { require(!snapshot.is_outdated) val name = snapshot.node_name if (plain_text) { val title = "File " + Symbol.cartouche_decoded(name.path.file_name) val body = HTML.text(snapshot.node.source) html_context.html_document(title, body) } 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 body = html_body(snapshot.xml_markup(elements = html_elements)) html_context.html_document(title, body) } } } /** PDF LaTeX documents **/ /* document info */ abstract class Document_Name { def name: String def path: Path = Path.basic(name) override def toString: String = name } object Document_Variant { def parse(name: String, tags: String): Document_Variant = Document_Variant(name, Library.space_explode(',', tags)) def parse(opt: String): Document_Variant = Library.space_explode('=', opt) match { case List(name) => Document_Variant(name, Nil) case List(name, tags) => parse(name, tags) case _ => error("Malformed document variant: " + quote(opt)) } } sealed case class Document_Variant(name: String, tags: List[String]) extends Document_Name { def print_tags: String = tags.mkString(",") def print: String = if (tags.isEmpty) name else name + "=" + print_tags def latex_sty: String = Library.terminate_lines( tags.map(tag => tag.toList match { case '/' :: cs => "\\isafoldtag{" + cs.mkString + "}" case '-' :: cs => "\\isadroptag{" + cs.mkString + "}" case '+' :: cs => "\\isakeeptag{" + cs.mkString + "}" case cs => "\\isakeeptag{" + cs.mkString + "}" })) } sealed case class Document_Input(name: String, sources: SHA1.Digest) extends Document_Name sealed case class Document_Output(name: String, sources: SHA1.Digest, log_xz: Bytes, pdf: Bytes) extends Document_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) } /* 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(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(sources), log_xz, pdf)) } else None }) } def write_document(db: SQL.Database, session_name: String, doc: Document_Output) { 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() }) } /* presentation context */ object Context { val none: Context = new Context { def enabled: Boolean = false } val standard: Context = new Context { def enabled: Boolean = true } def dir(path: Path): Context = new Context { def enabled: Boolean = true override def dir(store: Sessions.Store): Path = path } def make(s: String): Context = if (s == ":") standard else dir(Path.explode(s)) } abstract class Context private { def enabled: Boolean def enabled(info: Sessions.Info): Boolean = enabled || info.browser_info def dir(store: Sessions.Store): Path = store.presentation_dir def dir(store: Sessions.Store, info: Sessions.Info): Path = dir(store) + Path.explode(info.chapter_session) } /** HTML presentation **/ /* maintain chapter index */ private val sessions_path = Path.basic(".sessions") private def read_sessions(dir: Path): List[(String, String)] = { val path = dir + sessions_path if (path.is_file) { import XML.Decode._ list(pair(string, string))(Symbol.decode_yxml(File.read(path))) } else Nil } private def write_sessions(dir: Path, sessions: List[(String, String)]) { import XML.Encode._ File.write(dir + sessions_path, YXML.string_of_body(list(pair(string, string))(sessions))) } def update_chapter_index(browser_info: Path, chapter: String, new_sessions: List[(String, String)]) { val dir = Isabelle_System.make_directory(browser_info + Path.basic(chapter)) val sessions0 = try { read_sessions(dir) } catch { case _: XML.Error => Nil } val sessions = (SortedMap.empty[String, String] ++ sessions0 ++ new_sessions).toList write_sessions(dir, sessions) val title = "Isabelle/" + chapter + " sessions" HTML.write_document(dir, "index.html", List(HTML.title(title + " (" + Distribution.version + ")")), HTML.chapter(title) :: (if (sessions.isEmpty) Nil else List(HTML.div("sessions", List(HTML.description( sessions.map({ case (name, description) => val descr = Symbol.trim_blank_lines(description) (List(HTML.link(name + "/index.html", HTML.text(name))), if (descr == "") Nil else HTML.break ::: List(HTML.pre(HTML.text(descr)))) }))))))) } def make_global_index(browser_info: Path) { if (!(browser_info + Path.explode("index.html")).is_file) { Isabelle_System.make_directory(browser_info) File.copy(Path.explode("~~/lib/logo/isabelle.gif"), browser_info + Path.explode("isabelle.gif")) File.write(browser_info + Path.explode("index.html"), File.read(Path.explode("~~/lib/html/library_index_header.template")) + File.read(Path.explode("~~/lib/html/library_index_content.template")) + File.read(Path.explode("~~/lib/html/library_index_footer.template"))) } } /* present session */ val session_graph_path = Path.explode("session_graph.pdf") val readme_path = Path.explode("README.html") val files_path = Path.explode("files") def html_name(name: Document.Node.Name): String = name.theory_base_name + ".html" def token_markups(keywords: Keyword.Keywords, tok: Token): List[String] = { if (keywords.is_command(tok, Keyword.theory_end)) List(Markup.KEYWORD2, Markup.KEYWORD) else if (keywords.is_command(tok, Keyword.proof_asm)) List(Markup.KEYWORD3, Markup.COMMAND) else if (keywords.is_command(tok, Keyword.improper)) List(Markup.KEYWORD1, Markup.IMPROPER, Markup.COMMAND) else if (tok.is_command) List(Markup.KEYWORD1, Markup.COMMAND) else if (tok.is_delimiter) List(Markup.DELIMITER, Markup.KEYWORD) else if (tok.is_keyword) List(Markup.KEYWORD2, Markup.KEYWORD) else if (tok.is_comment) List(Markup.COMMENT) else { tok.kind match { case Token.Kind.VAR => List(Markup.VAR) case Token.Kind.TYPE_IDENT => List(Markup.TFREE) case Token.Kind.TYPE_VAR => List(Markup.TVAR) case Token.Kind.STRING => List(Markup.STRING) case Token.Kind.ALT_STRING => List(Markup.ALT_STRING) case Token.Kind.VERBATIM => List(Markup.VERBATIM) case Token.Kind.CARTOUCHE => List(Markup.CARTOUCHE) case _ => Nil } } } def session_html( resources: Resources, session: String, deps: Sessions.Deps, db_context: Sessions.Database_Context, progress: Progress = new Progress, verbose: Boolean = false, html_context: HTML_Context, presentation: Context) { val info = deps.sessions_structure(session) val options = info.options val base = deps(session) val session_dir = presentation.dir(db_context.store, info) html_context.init_fonts(session_dir) Bytes.write(session_dir + session_graph_path, graphview.Graph_File.make_pdf(options, base.session_graph_display)) val documents = for { doc <- info.document_variants document <- db_context.input_database(session)(read_document(_, _, doc.name)) } yield { if (verbose) progress.echo("Presenting document " + session + "/" + doc.name) Bytes.write(session_dir + doc.path.pdf, document.pdf) doc } val links = { val deps_link = HTML.link(session_graph_path, HTML.text("theory dependencies")) val readme_links = if ((info.dir + readme_path).is_file) { File.copy(info.dir + readme_path, session_dir + readme_path) List(HTML.link(readme_path, HTML.text("README"))) } else Nil val document_links = documents.map(doc => HTML.link(doc.path.pdf, HTML.text(doc.name))) Library.separate(HTML.break ::: HTML.nl, (deps_link :: readme_links ::: document_links). map(link => HTML.text("View ") ::: List(link))).flatten } def theory_link(name1: Document.Node.Name, body: XML.Body): XML.Tree = { val session1 = base.theory_qualifier(name1) val info1 = deps.sessions_structure(session1) val prefix = if (session == session1) "" else if (info.chapter == info1.chapter) "../" + session1 + "/" else "../../" + info1.chapter_session + "/" HTML.link(prefix + html_name(name1), body) } val theories: List[XML.Body] = { var seen_files = List.empty[(Path, String, Document.Node.Name)] for (thy_name <- base.session_theories) yield { progress.expose_interrupt() if (verbose) progress.echo("Presenting theory " + thy_name) val syntax = base.theory_syntax(thy_name) val keywords = syntax.keywords val spans = syntax.parse_spans(Symbol.decode(File.read(thy_name.path))) val thy_body = { val imports_offset = base.known_theories(thy_name.theory).header.imports_offset var token_offset = 1 spans.flatMap(span => { val is_init = span.is_kind(keywords, Keyword.theory_begin, false) span.content.flatMap(tok => { val text = HTML.text(tok.source) val item = if (is_init && imports_offset.isDefinedAt(token_offset)) { List(theory_link(imports_offset(token_offset), text)) } else text token_offset += tok.symbol_length (token_markups(keywords, tok) :\ item)( { case (c, body) => List(HTML.span(c, body)) }) }) }) } val files = (for { thy_command <- Build_Job.read_theory(db_context, resources, session, thy_name.theory).iterator snapshot = Document.State.init.snippet(thy_command) (src_path, xml) <- snapshot.xml_markup_blobs(elements = html_elements).iterator if xml.nonEmpty } yield { progress.expose_interrupt() val file_name = (files_path + src_path.squash.html).implode seen_files.find(p => p._1 == src_path || p._2 == file_name) match { case None => seen_files ::= (src_path, file_name, thy_name) case Some((_, _, thy_name1)) => error("Incoherent use of file name " + src_path + " as " + quote(file_name) + " in theory " + thy_name1 + " vs. " + thy_name) } if (verbose) progress.echo("Presenting file " + src_path) val file_path = session_dir + Path.explode(file_name) html_context.init_fonts(file_path.dir) val file_title = "File " + Symbol.cartouche_decoded(src_path.implode_short) HTML.write_document(file_path.dir, file_path.file_name, List(HTML.title(file_title)), List(html_context.head(file_title), html_context.source(html_body(xml)))) List(HTML.link(file_name, HTML.text(file_title))) }).toList val thy_title = "Theory " + thy_name.theory_base_name HTML.write_document(session_dir, html_name(thy_name), List(HTML.title(thy_title)), List(html_context.head(thy_title), html_context.source(thy_body))) List(HTML.link(html_name(thy_name), HTML.text(thy_name.theory_base_name) ::: (if (files.isEmpty) Nil else List(HTML.itemize(files))))) } } val title = "Session " + session HTML.write_document(session_dir, "index.html", List(HTML.title(title + " (" + Distribution.version + ")")), html_context.head(title, List(HTML.par(links))) :: html_context.contents("Theories", theories)) } /** build documents **/ val session_tex_path = Path.explode("session.tex") def tex_name(name: Document.Node.Name): String = name.theory_base_name + ".tex" def document_tex_name(name: Document.Node.Name): String = "document/" + tex_name(name) class Build_Error(val log_lines: List[String], val message: String) extends Exn.User_Error(message) def build_documents( session: String, deps: Sessions.Deps, db_context: Sessions.Database_Context, progress: Progress = new Progress, output_sources: Option[Path] = None, output_pdf: Option[Path] = None, verbose: Boolean = false, verbose_latex: Boolean = false): List[Document_Output] = { /* session info */ val info = deps.sessions_structure(session) val hierarchy = deps.sessions_structure.hierarchy(session) val options = info.options val base = deps(session) val graph_pdf = graphview.Graph_File.make_pdf(options, base.session_graph_display) /* prepare document directory */ lazy val tex_files = for (name <- base.session_theories ::: base.document_theories) yield { val entry = db_context.get_export(hierarchy, name.theory, document_tex_name(name)) Path.basic(tex_name(name)) -> entry.uncompressed } def prepare_dir1(dir: Path, doc: Document_Variant): (Path, String) = { val doc_dir = dir + Path.basic(doc.name) Isabelle_System.make_directory(doc_dir) Isabelle_System.bash("isabelle latex -o sty", cwd = doc_dir.file).check File.write(doc_dir + Path.explode("isabelletags.sty"), doc.latex_sty) for ((base_dir, src) <- info.document_files) File.copy_base(info.dir + base_dir, src, doc_dir) File.write(doc_dir + session_tex_path, Library.terminate_lines( base.session_theories.map(name => "\\input{" + tex_name(name) + "}"))) for ((path, tex) <- tex_files) Bytes.write(doc_dir + path, tex) val root1 = "root_" + doc.name val root = if ((doc_dir + Path.explode(root1).tex).is_file) root1 else "root" (doc_dir, root) } def prepare_dir2(dir: Path, doc: Document_Variant): Unit = { val doc_dir = dir + Path.basic(doc.name) // non-deterministic, but irrelevant Bytes.write(doc_dir + session_graph_path, graph_pdf) } /* produce documents */ val documents = for (doc <- info.documents) yield { Isabelle_System.with_tmp_dir("document")(tmp_dir => { progress.echo("Preparing " + session + "/" + doc.name + " ...") val start = Time.now() // prepare sources val (doc_dir, root) = prepare_dir1(tmp_dir, doc) val digests = File.find_files(doc_dir.file, follow_links = true).map(SHA1.digest) val sources = SHA1.digest_set(digests) prepare_dir2(tmp_dir, doc) for (dir <- output_sources) { prepare_dir1(dir, doc) prepare_dir2(dir, doc) } // old document from database val old_document = for { old_doc <- db_context.input_database(session)(read_document(_, _, doc.name)) if old_doc.sources == sources } yield { Bytes.write(doc_dir + doc.path.pdf, old_doc.pdf) old_doc } old_document getOrElse { // bash scripts def root_bash(ext: String): String = Bash.string(root + "." + ext) def latex_bash(fmt: String = "pdf", ext: String = "tex"): String = "isabelle latex -o " + Bash.string(fmt) + " " + Bash.string(root + "." + ext) def bash(items: String*): Process_Result = progress.bash(items.mkString(" && "), cwd = doc_dir.file, echo = verbose_latex, watchdog = Time.seconds(0.5)) // prepare document val result = if ((doc_dir + Path.explode("build")).is_file) { bash("./build pdf " + Bash.string(doc.name)) } else { bash( latex_bash(), "{ [ ! -f " + root_bash("bib") + " ] || " + latex_bash("bbl") + "; }", "{ [ ! -f " + root_bash("idx") + " ] || " + latex_bash("idx") + "; }", latex_bash(), latex_bash()) } // result val root_pdf = Path.basic(root).pdf val result_path = doc_dir + root_pdf val log_lines = result.out_lines ::: result.err_lines if (!result.ok) { val message = Exn.cat_message( Library.trim_line(result.err), cat_lines(Latex.latex_errors(doc_dir, root) ::: Bibtex.bibtex_errors(doc_dir, root)), "Failed to build document " + quote(doc.name)) throw new Build_Error(log_lines, message) } else if (!result_path.is_file) { val message = "Bad document result: expected to find " + root_pdf throw new Build_Error(log_lines, message) } else { val stop = Time.now() val timing = stop - start progress.echo("Finished " + session + "/" + doc.name + " (" + timing.message_hms + " elapsed time)") val log_xz = Bytes(cat_lines(log_lines)).compress() val pdf = Bytes.read(result_path) Document_Output(doc.name, sources, log_xz, pdf) } } }) } for (dir <- output_pdf; doc <- documents) { Isabelle_System.make_directory(dir) val path = dir + doc.path.pdf Bytes.write(path, doc.pdf) 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) val store = Sessions.store(options) progress.interrupt_handler { val res = Build.build(options, selection = Sessions.Selection.session(session), dirs = dirs, progress = progress, verbose = verbose_build) if (!res.ok) error("Failed to build session " + quote(session)) val deps = Sessions.load_structure(options + "document=pdf", dirs = dirs). selection_deps(Sessions.Selection.session(session)) if (output_sources.isEmpty && output_pdf.isEmpty) { progress.echo_warning("No output directory") } using(store.open_database_context())(db_context => build_documents(session, deps, db_context, progress = progress, output_sources = output_sources, output_pdf = output_pdf, verbose = true, verbose_latex = verbose_latex)) } }) }