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 ++= ""; s ++= markup.name; 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 ++= ""; s ++= elem; 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 ++= ""; s ++= markup.name; 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))
}
})
}