diff --git a/src/Pure/Thy/export.scala b/src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala
+++ b/src/Pure/Thy/export.scala
@@ -1,571 +1,572 @@
/* Title: Pure/Thy/export.scala
Author: Makarius
Manage theory exports: compressed blobs.
*/
package isabelle
import scala.annotation.tailrec
import scala.util.matching.Regex
object Export {
/* artefact names */
val DOCUMENT_ID = "PIDE/document_id"
val FILES = "PIDE/files"
val MARKUP = "PIDE/markup"
val MESSAGES = "PIDE/messages"
val DOCUMENT_PREFIX = "document/"
val DOCUMENT_LATEX = DOCUMENT_PREFIX + "latex"
val DOCUMENT_CITATIONS = DOCUMENT_PREFIX + "citations"
val THEORY_PREFIX: String = "theory/"
val PROOFS_PREFIX: String = "proofs/"
val THEORY_PARENTS: String = THEORY_PREFIX + "parents"
def explode_name(s: String): List[String] = space_explode('/', s)
def implode_name(elems: Iterable[String]): String = elems.mkString("/")
/* SQL data model */
object Data {
val session_name = SQL.Column.string("session_name").make_primary_key
val theory_name = SQL.Column.string("theory_name").make_primary_key
val name = SQL.Column.string("name").make_primary_key
val executable = SQL.Column.bool("executable")
val compressed = SQL.Column.bool("compressed")
val body = SQL.Column.bytes("body")
val table =
SQL.Table("isabelle_exports",
List(session_name, theory_name, name, executable, compressed, body))
def where_equal(session_name: String, theory_name: String = "", name: String = ""): SQL.Source =
"WHERE " + Data.session_name.equal(session_name) +
(if (theory_name == "") "" else " AND " + Data.theory_name.equal(theory_name)) +
(if (name == "") "" else " AND " + Data.name.equal(name))
}
def compound_name(a: String, b: String): String =
if (a.isEmpty) b else a + ":" + b
sealed case class Entry_Name(session: String = "", theory: String = "", name: String = "") {
val compound_name: String = Export.compound_name(theory, name)
def make_path(prune: Int = 0): Path = {
val elems = theory :: space_explode('/', name)
if (elems.length < prune + 1) {
error("Cannot prune path by " + prune + " element(s): " + Path.make(elems))
}
else Path.make(elems.drop(prune))
}
def readable(db: SQL.Database): Boolean = {
val select = Data.table.select(List(Data.name), Data.where_equal(session, theory, name))
db.using_statement(select)(stmt => stmt.execute_query().next())
}
def read(db: SQL.Database, cache: XML.Cache): Option[Entry] = {
val select =
Data.table.select(List(Data.executable, Data.compressed, Data.body),
Data.where_equal(session, theory, name))
db.using_statement(select) { stmt =>
val res = stmt.execute_query()
if (res.next()) {
val executable = res.bool(Data.executable)
val compressed = res.bool(Data.compressed)
val bytes = res.bytes(Data.body)
val body = Future.value(compressed, bytes)
Some(Entry(this, executable, body, cache))
}
else None
}
}
}
def read_theory_names(db: SQL.Database, session_name: String): List[String] = {
val select =
Data.table.select(List(Data.theory_name),
Data.where_equal(session_name, name = THEORY_PARENTS)) +
" ORDER BY " + Data.theory_name
db.using_statement(select)(stmt =>
stmt.execute_query().iterator(_.string(Data.theory_name)).toList)
}
def read_entry_names(db: SQL.Database, session_name: String): List[Entry_Name] = {
val select =
Data.table.select(List(Data.theory_name, Data.name), Data.where_equal(session_name)) +
" ORDER BY " + Data.theory_name + ", " + Data.name
db.using_statement(select)(stmt =>
stmt.execute_query().iterator(res =>
Entry_Name(session = session_name,
theory = res.string(Data.theory_name),
name = res.string(Data.name))).toList)
}
def message(msg: String, theory_name: String, name: String): String =
msg + " " + quote(name) + " for theory " + quote(theory_name)
def empty_entry(theory_name: String, name: String): Entry =
Entry(Entry_Name(theory = theory_name, name = name),
false, Future.value(false, Bytes.empty), XML.Cache.none)
sealed case class Entry(
entry_name: Entry_Name,
executable: Boolean,
body: Future[(Boolean, Bytes)],
cache: XML.Cache
) {
def session_name: String = entry_name.session
def theory_name: String = entry_name.theory
def name: String = entry_name.name
override def toString: String = name
def compound_name: String = entry_name.compound_name
def name_has_prefix(s: String): Boolean = name.startsWith(s)
val name_elems: List[String] = explode_name(name)
def name_extends(elems: List[String]): Boolean =
name_elems.startsWith(elems) && name_elems != elems
def text: String = uncompressed.text
def uncompressed: Bytes = {
val (compressed, bytes) = body.join
if (compressed) bytes.uncompress(cache = cache.xz) else bytes
}
def uncompressed_yxml: XML.Body =
YXML.parse_body(UTF8.decode_permissive(uncompressed), cache = cache)
def write(db: SQL.Database): Unit = {
val (compressed, bytes) = body.join
db.using_statement(Data.table.insert()) { stmt =>
stmt.string(1) = session_name
stmt.string(2) = theory_name
stmt.string(3) = name
stmt.bool(4) = executable
stmt.bool(5) = compressed
stmt.bytes(6) = bytes
stmt.execute()
}
}
}
def make_regex(pattern: String): Regex = {
@tailrec def make(result: List[String], depth: Int, chs: List[Char]): Regex =
chs match {
case '*' :: '*' :: rest => make("[^:]*" :: result, depth, rest)
case '*' :: rest => make("[^:/]*" :: result, depth, rest)
case '?' :: rest => make("[^:/]" :: result, depth, rest)
case '\\' :: c :: rest => make(("\\" + c) :: result, depth, rest)
case '{' :: rest => make("(" :: result, depth + 1, rest)
case ',' :: rest if depth > 0 => make("|" :: result, depth, rest)
case '}' :: rest if depth > 0 => make(")" :: result, depth - 1, rest)
case c :: rest if ".+()".contains(c) => make(("\\" + c) :: result, depth, rest)
case c :: rest => make(c.toString :: result, depth, rest)
case Nil => result.reverse.mkString.r
}
make(Nil, 0, pattern.toList)
}
def make_matcher(pats: List[String]): Entry_Name => Boolean = {
val regs = pats.map(make_regex)
(entry_name: Entry_Name) =>
regs.exists(_.pattern.matcher(entry_name.compound_name).matches)
}
def make_entry(
session_name: String,
args: Protocol.Export.Args,
bytes: Bytes,
cache: XML.Cache
): Entry = {
val body =
if (args.compress) Future.fork(bytes.maybe_compress(cache = cache.xz))
else Future.value((false, bytes))
val entry_name = Entry_Name(session = session_name, theory = args.theory_name, name = args.name)
Entry(entry_name, args.executable, body, cache)
}
/* database consumer thread */
def consumer(db: SQL.Database, cache: XML.Cache, progress: Progress = new Progress): Consumer =
new Consumer(db, cache, progress)
class Consumer private[Export](db: SQL.Database, cache: XML.Cache, progress: Progress) {
private val errors = Synchronized[List[String]](Nil)
private val consumer =
Consumer_Thread.fork_bulk[(Entry, Boolean)](name = "export")(
bulk = { case (entry, _) => entry.body.is_finished },
consume =
{ (args: List[(Entry, Boolean)]) =>
val results =
db.transaction {
for ((entry, strict) <- args)
yield {
if (progress.stopped) {
entry.body.cancel()
Exn.Res(())
}
else if (entry.entry_name.readable(db)) {
if (strict) {
val msg = message("Duplicate export", entry.theory_name, entry.name)
errors.change(msg :: _)
}
Exn.Res(())
}
else Exn.capture { entry.write(db) }
}
}
(results, true)
})
def make_entry(session_name: String, args: Protocol.Export.Args, body: Bytes): Unit = {
if (!progress.stopped && !body.is_empty) {
consumer.send(Export.make_entry(session_name, args, body, cache) -> args.strict)
}
}
def shutdown(close: Boolean = false): List[String] = {
consumer.shutdown()
if (close) db.close()
errors.value.reverse ::: (if (progress.stopped) List("Export stopped") else Nil)
}
}
/* context for database access */
def open_database_context(store: Sessions.Store): Database_Context = {
val database_server = if (store.database_server) Some(store.open_database_server()) else None
new Database_Context(store, database_server)
}
def open_session_context0(store: Sessions.Store, session: String): Session_Context =
open_database_context(store).open_session0(session, close_database_context = true)
def open_session_context(
store: Sessions.Store,
session_base_info: Sessions.Base_Info,
document_snapshot: Option[Document.Snapshot] = None
): Session_Context = {
open_database_context(store).open_session(
session_base_info, document_snapshot = document_snapshot, close_database_context = true)
}
class Database_Context private[Export](
val store: Sessions.Store,
val database_server: Option[SQL.Database]
) extends AutoCloseable {
database_context =>
override def toString: String = {
val s =
database_server match {
case Some(db) => db.toString
case None => "input_dirs = " + store.input_dirs.map(_.absolute).mkString(", ")
}
"Database_Context(" + s + ")"
}
def cache: Term.Cache = store.cache
def close(): Unit = database_server.foreach(_.close())
def open_output_database(session: String): Session_Database =
database_server match {
case Some(db) => new Session_Database(session, db)
case None =>
new Session_Database(session, store.open_database(session, output = true)) {
override def close(): Unit = db.close()
}
}
def open_session0(session: String, close_database_context: Boolean = false): Session_Context =
open_session(Sessions.base_info0(session), close_database_context = close_database_context)
def open_session(
session_base_info: Sessions.Base_Info,
document_snapshot: Option[Document.Snapshot] = None,
close_database_context: Boolean = false
): Session_Context = {
val session_name = session_base_info.check.base.session_name
val session_hierarchy = session_base_info.sessions_structure.build_hierarchy(session_name)
val session_databases =
database_server match {
case Some(db) => session_hierarchy.map(name => new Session_Database(name, db))
case None =>
val attempts =
session_hierarchy.map(name => name -> store.try_open_database(name, server = false))
attempts.collectFirst({ case (name, None) => name }) match {
case Some(bad) =>
for ((_, Some(db)) <- attempts) db.close()
store.bad_database(bad)
case None =>
for ((name, Some(db)) <- attempts) yield {
new Session_Database(name, db) { override def close(): Unit = this.db.close() }
}
}
}
new Session_Context(database_context, session_base_info, session_databases, document_snapshot) {
override def close(): Unit = {
session_databases.foreach(_.close())
if (close_database_context) database_context.close()
}
}
}
}
class Session_Database private[Export](val session: String, val db: SQL.Database)
extends AutoCloseable {
def close(): Unit = ()
lazy private [Export] val theory_names: List[String] = read_theory_names(db, session)
lazy private [Export] val entry_names: List[Entry_Name] = read_entry_names(db, session)
}
class Session_Context private[Export](
val database_context: Database_Context,
session_base_info: Sessions.Base_Info,
db_hierarchy: List[Session_Database],
document_snapshot: Option[Document.Snapshot]
) extends AutoCloseable {
session_context =>
def close(): Unit = ()
def cache: Term.Cache = database_context.cache
def sessions_structure: Sessions.Structure = session_base_info.sessions_structure
def session_base: Sessions.Base = session_base_info.base
def session_name: String =
if (document_snapshot.isDefined) Sessions.DRAFT
else session_base.session_name
def session_database(session: String = session_name): Option[Session_Database] =
db_hierarchy.find(_.session == session)
def session_db(session: String = session_name): Option[SQL.Database] =
session_database(session = session).map(_.db)
def session_stack: List[String] =
((if (document_snapshot.isDefined) List(session_name) else Nil) :::
db_hierarchy.map(_.session)).reverse
private def select[A](
session: String,
select1: Entry_Name => Option[A],
select2: Session_Database => List[A]
): List[A] = {
def sel(name: String): List[A] =
if (name == Sessions.DRAFT) {
(for {
snapshot <- document_snapshot.iterator
entry_name <- snapshot.all_exports.keysIterator
res <- select1(entry_name).iterator
} yield entry_name -> res).toList.sortBy(_._1.compound_name).map(_._2)
}
else { session_database(name).map(select2).getOrElse(Nil) }
if (session.nonEmpty) sel(session) else session_stack.flatMap(sel)
}
def entry_names(session: String = session_name): List[Entry_Name] =
select(session, Some(_), _.entry_names)
def theory_names(session: String = session_name): List[String] =
select(session, a => if(a.name == THEORY_PARENTS) Some(a.theory) else None, _.theory_names)
def get(theory: String, name: String): Option[Entry] =
{
def snapshot_entry: Option[Entry] =
for {
snapshot <- document_snapshot
entry_name = Entry_Name(session = Sessions.DRAFT, theory = theory, name = name)
entry <- snapshot.all_exports.get(entry_name)
} yield entry
def db_entry: Option[Entry] =
db_hierarchy.view.map(database =>
Export.Entry_Name(session = database.session, theory = theory, name = name)
.read(database.db, cache))
.collectFirst({ case Some(entry) => entry })
snapshot_entry orElse db_entry
}
def apply(theory: String, name: String, permissive: Boolean = false): Entry =
get(theory, name) match {
case None if permissive => empty_entry(theory, name)
case None => error("Missing export entry " + quote(compound_name(theory, name)))
case Some(entry) => entry
}
- def theory(theory: String): Theory_Context =
- new Theory_Context(session_context, theory)
+ def theory(theory: String, other_cache: Option[Term.Cache] = None): Theory_Context =
+ new Theory_Context(session_context, theory, other_cache)
def classpath(): List[File.Content_Bytes] = {
(for {
session <- session_stack.iterator
info <- sessions_structure.get(session).iterator
if info.export_classpath.nonEmpty
matcher = make_matcher(info.export_classpath)
entry_name <- entry_names(session = session).iterator
if matcher(entry_name)
entry <- get(entry_name.theory, entry_name.name).iterator
} yield File.Content(entry.entry_name.make_path(), entry.uncompressed)).toList
}
override def toString: String =
"Export.Session_Context(" + commas_quote(session_stack) + ")"
}
class Theory_Context private[Export](
val session_context: Session_Context,
- val theory: String
+ val theory: String,
+ other_cache: Option[Term.Cache]
) {
- def cache: Term.Cache = session_context.cache
+ def cache: Term.Cache = other_cache getOrElse session_context.cache
def get(name: String): Option[Entry] = session_context.get(theory, name)
def apply(name: String, permissive: Boolean = false): Entry =
session_context.apply(theory, name, permissive = permissive)
def uncompressed_yxml(name: String): XML.Body =
get(name) match {
case Some(entry) => entry.uncompressed_yxml
case None => Nil
}
def document_id(): Option[Long] =
apply(DOCUMENT_ID, permissive = true).text match {
case Value.Long(id) => Some(id)
case _ => None
}
def files(): Option[(String, List[String])] =
split_lines(apply(FILES, permissive = true).text) match {
case Nil => None
case thy_file :: blobs_files => Some((thy_file, blobs_files))
}
override def toString: String = "Export.Theory_Context(" + quote(theory) + ")"
}
/* export to file-system */
def export_files(
store: Sessions.Store,
session_name: String,
export_dir: Path,
progress: Progress = new Progress,
export_prune: Int = 0,
export_list: Boolean = false,
export_patterns: List[String] = Nil
): Unit = {
using(store.open_database(session_name)) { db =>
val entry_names = read_entry_names(db, session_name)
// list
if (export_list) {
for (entry_name <- entry_names) progress.echo(entry_name.compound_name)
}
// export
if (export_patterns.nonEmpty) {
val matcher = make_matcher(export_patterns)
for {
entry_name <- entry_names if matcher(entry_name)
entry <- entry_name.read(db, store.cache)
} {
val path = export_dir + entry_name.make_path(prune = export_prune)
progress.echo("export " + path + (if (entry.executable) " (executable)" else ""))
Isabelle_System.make_directory(path.dir)
val bytes = entry.uncompressed
if (!path.is_file || Bytes.read(path) != bytes) Bytes.write(path, bytes)
File.set_executable(path, entry.executable)
}
}
}
}
/* Isabelle tool wrapper */
val default_export_dir: Path = Path.explode("export")
val isabelle_tool =
Isabelle_Tool("export", "retrieve theory exports", Scala_Project.here,
{ args =>
/* arguments */
var export_dir = default_export_dir
var dirs: List[Path] = Nil
var export_list = false
var no_build = false
var options = Options.init()
var export_prune = 0
var export_patterns: List[String] = Nil
val getopts = Getopts("""
Usage: isabelle export [OPTIONS] SESSION
Options are:
-O DIR output directory for exported files (default: """ + default_export_dir + """)
-d DIR include session directory
-l list exports
-n no build of session
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-p NUM prune path of exported files by NUM elements
-x PATTERN extract files matching pattern (e.g. "*:**" for all)
List or export theory exports for SESSION: named blobs produced by
isabelle build. Option -l or -x is required; option -x may be repeated.
The PATTERN language resembles glob patterns in the shell, with ? and *
(both excluding ":" and "/"), ** (excluding ":"), and [abc] or [^abc],
and variants {pattern1,pattern2,pattern3}.
""",
"O:" -> (arg => export_dir = Path.explode(arg)),
"d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
"l" -> (_ => export_list = true),
"n" -> (_ => no_build = true),
"o:" -> (arg => options = options + arg),
"p:" -> (arg => export_prune = Value.Int.parse(arg)),
"x:" -> (arg => export_patterns ::= arg))
val more_args = getopts(args)
val session_name =
more_args match {
case List(session_name) if export_list || export_patterns.nonEmpty => session_name
case _ => getopts.usage()
}
val progress = new Console_Progress()
/* build */
if (!no_build) {
val rc =
progress.interrupt_handler {
Build.build_logic(options, session_name, progress = progress, dirs = dirs)
}
if (rc != Process_Result.RC.ok) sys.exit(rc)
}
/* export files */
val store = Sessions.store(options)
export_files(store, session_name, export_dir, progress = progress, export_prune = export_prune,
export_list = export_list, export_patterns = export_patterns)
})
}
diff --git a/src/Pure/Thy/export_theory.scala b/src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala
+++ b/src/Pure/Thy/export_theory.scala
@@ -1,751 +1,752 @@
/* Title: Pure/Thy/export_theory.scala
Author: Makarius
Export foundational theory content.
*/
package isabelle
import scala.collection.immutable.SortedMap
object Export_Theory {
/** session content **/
sealed case class Session(name: String, theory_graph: Graph[String, Option[Theory]]) {
override def toString: String = name
def theory(theory_name: String): Option[Theory] =
if (theory_graph.defined(theory_name)) theory_graph.get_node(theory_name)
else None
def theories: List[Theory] =
theory_graph.topological_order.flatMap(theory)
}
def read_session(
session_context: Export.Session_Context,
- progress: Progress = new Progress,
- cache: Term.Cache = Term.Cache.make()
+ progress: Progress = new Progress
): Session = {
val thys =
for (theory <- session_context.theory_names()) yield {
progress.echo("Reading theory " + theory)
- read_theory(session_context.theory(theory), cache = cache)
+ read_theory(session_context.theory(theory))
}
val graph0 =
thys.foldLeft(Graph.string[Option[Theory]]) {
case (g, thy) => g.default_node(thy.name, Some(thy))
}
val graph1 =
thys.foldLeft(graph0) {
case (g0, thy) =>
thy.parents.foldLeft(g0) {
case (g1, parent) => g1.default_node(parent, None).add_edge_acyclic(parent, thy.name)
}
}
Session(session_context.session_name, graph1)
}
/** theory content **/
sealed case class Theory(name: String, parents: List[String],
types: List[Entity[Type]],
consts: List[Entity[Const]],
axioms: List[Entity[Axiom]],
thms: List[Entity[Thm]],
classes: List[Entity[Class]],
locales: List[Entity[Locale]],
locale_dependencies: List[Entity[Locale_Dependency]],
classrel: List[Classrel],
arities: List[Arity],
constdefs: List[Constdef],
typedefs: List[Typedef],
datatypes: List[Datatype],
spec_rules: List[Spec_Rule],
others: Map[String, List[Entity[Other]]]
) {
override def toString: String = name
def entity_iterator: Iterator[Entity0] =
types.iterator.map(_.no_content) ++
consts.iterator.map(_.no_content) ++
axioms.iterator.map(_.no_content) ++
thms.iterator.map(_.no_content) ++
classes.iterator.map(_.no_content) ++
locales.iterator.map(_.no_content) ++
locale_dependencies.iterator.map(_.no_content) ++
(for { (_, xs) <- others; x <- xs.iterator } yield x.no_content)
def cache(cache: Term.Cache): Theory =
Theory(cache.string(name),
parents.map(cache.string),
types.map(_.cache(cache)),
consts.map(_.cache(cache)),
axioms.map(_.cache(cache)),
thms.map(_.cache(cache)),
classes.map(_.cache(cache)),
locales.map(_.cache(cache)),
locale_dependencies.map(_.cache(cache)),
classrel.map(_.cache(cache)),
arities.map(_.cache(cache)),
constdefs.map(_.cache(cache)),
typedefs.map(_.cache(cache)),
datatypes.map(_.cache(cache)),
spec_rules.map(_.cache(cache)),
(for ((k, xs) <- others.iterator) yield cache.string(k) -> xs.map(_.cache(cache))).toMap)
}
def read_theory_parents(theory_context: Export.Theory_Context): Option[List[String]] =
theory_context.get(Export.THEORY_PARENTS)
.map(entry => Library.trim_split_lines(entry.uncompressed.text))
def no_theory: Theory =
Theory("", Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Map.empty)
def read_theory(
theory_context: Export.Theory_Context,
- permissive: Boolean = false,
- cache: Term.Cache = Term.Cache.none
+ permissive: Boolean = false
): Theory = {
+ val cache = theory_context.cache
val session_name = theory_context.session_context.session_name
val theory_name = theory_context.theory
read_theory_parents(theory_context) match {
case None if permissive => no_theory
case None =>
error("Missing theory export in session " + quote(session_name) + ": " + quote(theory_name))
case Some(parents) =>
val theory =
Theory(theory_name, parents,
read_types(theory_context),
read_consts(theory_context),
read_axioms(theory_context),
read_thms(theory_context),
read_classes(theory_context),
read_locales(theory_context),
read_locale_dependencies(theory_context),
read_classrel(theory_context),
read_arities(theory_context),
read_constdefs(theory_context),
read_typedefs(theory_context),
read_datatypes(theory_context),
read_spec_rules(theory_context),
read_others(theory_context))
if (cache.no_cache) theory else theory.cache(cache)
}
}
/* entities */
object Kind {
val TYPE = "type"
val CONST = "const"
val THM = "thm"
val PROOF = "proof"
val LOCALE_DEPENDENCY = "locale_dependency"
val DOCUMENT_HEADING = "document_heading"
val DOCUMENT_TEXT = "document_text"
val PROOF_TEXT = "proof_text"
}
def export_kind(kind: String): String =
if (kind == Markup.TYPE_NAME) Kind.TYPE
else if (kind == Markup.CONSTANT) Kind.CONST
else kind
def export_kind_name(kind: String, name: String): String =
name + "|" + export_kind(kind)
abstract class Content[T] {
def cache(cache: Term.Cache): T
}
sealed case class No_Content() extends Content[No_Content] {
def cache(cache: Term.Cache): No_Content = this
}
sealed case class Entity[A <: Content[A]](
kind: String,
name: String,
xname: String,
pos: Position.T,
id: Option[Long],
serial: Long,
content: Option[A]
) {
val kname: String = export_kind_name(kind, name)
val range: Symbol.Range = Position.Range.unapply(pos).getOrElse(Text.Range.offside)
def export_kind: String = Export_Theory.export_kind(kind)
override def toString: String = export_kind + " " + quote(name)
def the_content: A =
if (content.isDefined) content.get else error("No content for " + toString)
def no_content: Entity0 = copy(content = None)
def cache(cache: Term.Cache): Entity[A] =
Entity(
cache.string(kind),
cache.string(name),
cache.string(xname),
cache.position(pos),
id,
serial,
content.map(_.cache(cache)))
}
type Entity0 = Entity[No_Content]
def read_entities[A <: Content[A]](
theory_context: Export.Theory_Context,
export_name: String,
kind: String,
decode: XML.Decode.T[A]
): List[Entity[A]] = {
def decode_entity(tree: XML.Tree): Entity[A] = {
def err(): Nothing = throw new XML.XML_Body(List(tree))
tree match {
case XML.Elem(Markup(Markup.ENTITY, props), body) =>
val name = Markup.Name.unapply(props) getOrElse err()
val xname = Markup.XName.unapply(props) getOrElse err()
val pos = props.filter(p => Markup.position_property(p) && p._1 != Markup.ID)
val id = Position.Id.unapply(props)
val serial = Markup.Serial.unapply(props) getOrElse err()
val content = if (body.isEmpty) None else Some(decode(body))
Entity(kind, name, xname, pos, id, serial, content)
case _ => err()
}
}
theory_context.uncompressed_yxml(export_name).map(decode_entity)
}
/* approximative syntax */
object Assoc extends Enumeration {
val NO_ASSOC, LEFT_ASSOC, RIGHT_ASSOC = Value
}
sealed abstract class Syntax
case object No_Syntax extends Syntax
case class Prefix(delim: String) extends Syntax
case class Infix(assoc: Assoc.Value, delim: String, pri: Int) extends Syntax
def decode_syntax: XML.Decode.T[Syntax] =
XML.Decode.variant(List(
{ case (Nil, Nil) => No_Syntax },
{ case (List(delim), Nil) => Prefix(delim) },
{ case (Nil, body) =>
import XML.Decode._
val (ass, delim, pri) = triple(int, string, int)(body)
Infix(Assoc(ass), delim, pri) }))
/* types */
sealed case class Type(syntax: Syntax, args: List[String], abbrev: Option[Term.Typ])
extends Content[Type] {
override def cache(cache: Term.Cache): Type =
Type(
syntax,
args.map(cache.string),
abbrev.map(cache.typ))
}
def read_types(theory_context: Export.Theory_Context): List[Entity[Type]] =
read_entities(theory_context, Export.THEORY_PREFIX + "types", Markup.TYPE_NAME,
{ body =>
import XML.Decode._
val (syntax, args, abbrev) =
triple(decode_syntax, list(string), option(Term_XML.Decode.typ))(body)
Type(syntax, args, abbrev)
})
/* consts */
sealed case class Const(
syntax: Syntax,
typargs: List[String],
typ: Term.Typ,
abbrev: Option[Term.Term],
propositional: Boolean
) extends Content[Const] {
override def cache(cache: Term.Cache): Const =
Const(
syntax,
typargs.map(cache.string),
cache.typ(typ),
abbrev.map(cache.term),
propositional)
}
def read_consts(theory_context: Export.Theory_Context): List[Entity[Const]] =
read_entities(theory_context, Export.THEORY_PREFIX + "consts", Markup.CONSTANT,
{ body =>
import XML.Decode._
val (syntax, (typargs, (typ, (abbrev, propositional)))) =
pair(decode_syntax,
pair(list(string),
pair(Term_XML.Decode.typ,
pair(option(Term_XML.Decode.term), bool))))(body)
Const(syntax, typargs, typ, abbrev, propositional)
})
/* axioms */
sealed case class Prop(
typargs: List[(String, Term.Sort)],
args: List[(String, Term.Typ)],
term: Term.Term
) extends Content[Prop] {
override def cache(cache: Term.Cache): Prop =
Prop(
typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
cache.term(term))
}
def decode_prop(body: XML.Body): Prop = {
val (typargs, args, t) = {
import XML.Decode._
import Term_XML.Decode._
triple(list(pair(string, sort)), list(pair(string, typ)), term)(body)
}
Prop(typargs, args, t)
}
sealed case class Axiom(prop: Prop) extends Content[Axiom] {
override def cache(cache: Term.Cache): Axiom = Axiom(prop.cache(cache))
}
def read_axioms(theory_context: Export.Theory_Context): List[Entity[Axiom]] =
read_entities(theory_context, Export.THEORY_PREFIX + "axioms", Markup.AXIOM,
body => Axiom(decode_prop(body)))
/* theorems */
sealed case class Thm_Id(serial: Long, theory_name: String)
sealed case class Thm(
prop: Prop,
deps: List[String],
proof: Term.Proof)
extends Content[Thm] {
override def cache(cache: Term.Cache): Thm =
Thm(
prop.cache(cache),
deps.map(cache.string),
cache.proof(proof))
}
def read_thms(theory_context: Export.Theory_Context): List[Entity[Thm]] =
read_entities(theory_context, Export.THEORY_PREFIX + "thms", Kind.THM,
{ body =>
import XML.Decode._
import Term_XML.Decode._
val (prop, deps, prf) = triple(decode_prop, list(string), proof)(body)
Thm(prop, deps, prf)
})
sealed case class Proof(
typargs: List[(String, Term.Sort)],
args: List[(String, Term.Typ)],
term: Term.Term,
proof: Term.Proof
) {
def prop: Prop = Prop(typargs, args, term)
def cache(cache: Term.Cache): Proof =
Proof(
typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
cache.term(term),
cache.proof(proof))
}
def read_proof(
session_context: Export.Session_Context,
id: Thm_Id,
- cache: Term.Cache = Term.Cache.none
+ other_cache: Option[Term.Cache] = None
): Option[Proof] = {
- val theory_context = session_context.theory(id.theory_name)
+ val theory_context = session_context.theory(id.theory_name, other_cache = other_cache)
+ val cache = theory_context.cache
+
for { entry <- theory_context.get(Export.PROOFS_PREFIX + id.serial) }
yield {
val body = entry.uncompressed_yxml
val (typargs, (args, (prop_body, proof_body))) = {
import XML.Decode._
import Term_XML.Decode._
pair(list(pair(string, sort)), pair(list(pair(string, typ)), pair(x => x, x => x)))(body)
}
val env = args.toMap
val prop = Term_XML.Decode.term_env(env)(prop_body)
val proof = Term_XML.Decode.proof_env(env)(proof_body)
val result = Proof(typargs, args, prop, proof)
if (cache.no_cache) result else result.cache(cache)
}
}
def read_proof_boxes(
session_context: Export.Session_Context,
proof: Term.Proof,
suppress: Thm_Id => Boolean = _ => false,
- cache: Term.Cache = Term.Cache.none
+ other_cache: Option[Term.Cache] = None
): List[(Thm_Id, Proof)] = {
var seen = Set.empty[Long]
var result = SortedMap.empty[Long, (Thm_Id, Proof)]
def boxes(context: Option[(Long, Term.Proof)], prf: Term.Proof): Unit = {
prf match {
case Term.Abst(_, _, p) => boxes(context, p)
case Term.AbsP(_, _, p) => boxes(context, p)
case Term.Appt(p, _) => boxes(context, p)
case Term.AppP(p, q) => boxes(context, p); boxes(context, q)
case thm: Term.PThm if !seen(thm.serial) =>
seen += thm.serial
val id = Thm_Id(thm.serial, thm.theory_name)
if (!suppress(id)) {
- Export_Theory.read_proof(session_context, id, cache = cache) match {
+ Export_Theory.read_proof(session_context, id, other_cache = other_cache) match {
case Some(p) =>
result += (thm.serial -> (id -> p))
boxes(Some((thm.serial, p.proof)), p.proof)
case None =>
error("Missing proof " + thm.serial + " (theory " + quote (thm.theory_name) + ")" +
(context match {
case None => ""
case Some((i, p)) => " in proof " + i + ":\n" + p
}))
}
}
case _ =>
}
}
boxes(None, proof)
result.iterator.map(_._2).toList
}
/* type classes */
sealed case class Class(params: List[(String, Term.Typ)], axioms: List[Prop])
extends Content[Class] {
override def cache(cache: Term.Cache): Class =
Class(
params.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
axioms.map(_.cache(cache)))
}
def read_classes(theory_context: Export.Theory_Context): List[Entity[Class]] =
read_entities(theory_context, Export.THEORY_PREFIX + "classes", Markup.CLASS,
{ body =>
import XML.Decode._
import Term_XML.Decode._
val (params, axioms) = pair(list(pair(string, typ)), list(decode_prop))(body)
Class(params, axioms)
})
/* locales */
sealed case class Locale(
typargs: List[(String, Term.Sort)],
args: List[((String, Term.Typ), Syntax)],
axioms: List[Prop]
) extends Content[Locale] {
override def cache(cache: Term.Cache): Locale =
Locale(
typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
args.map({ case ((name, typ), syntax) => ((cache.string(name), cache.typ(typ)), syntax) }),
axioms.map(_.cache(cache)))
}
def read_locales(theory_context: Export.Theory_Context): List[Entity[Locale]] =
read_entities(theory_context, Export.THEORY_PREFIX + "locales", Markup.LOCALE,
{ body =>
import XML.Decode._
import Term_XML.Decode._
val (typargs, args, axioms) =
triple(list(pair(string, sort)), list(pair(pair(string, typ), decode_syntax)),
list(decode_prop))(body)
Locale(typargs, args, axioms)
})
/* locale dependencies */
sealed case class Locale_Dependency(
source: String,
target: String,
prefix: List[(String, Boolean)],
subst_types: List[((String, Term.Sort), Term.Typ)],
subst_terms: List[((String, Term.Typ), Term.Term)]
) extends Content[Locale_Dependency] {
override def cache(cache: Term.Cache): Locale_Dependency =
Locale_Dependency(
cache.string(source),
cache.string(target),
prefix.map({ case (name, mandatory) => (cache.string(name), mandatory) }),
subst_types.map({ case ((a, s), ty) => ((cache.string(a), cache.sort(s)), cache.typ(ty)) }),
subst_terms.map({ case ((x, ty), t) => ((cache.string(x), cache.typ(ty)), cache.term(t)) }))
def is_inclusion: Boolean =
subst_types.isEmpty && subst_terms.isEmpty
}
def read_locale_dependencies(
theory_context: Export.Theory_Context
): List[Entity[Locale_Dependency]] = {
read_entities(theory_context, Export.THEORY_PREFIX + "locale_dependencies",
Kind.LOCALE_DEPENDENCY,
{ body =>
import XML.Decode._
import Term_XML.Decode._
val (source, (target, (prefix, (subst_types, subst_terms)))) =
pair(string, pair(string, pair(list(pair(string, bool)),
pair(list(pair(pair(string, sort), typ)), list(pair(pair(string, typ), term))))))(body)
Locale_Dependency(source, target, prefix, subst_types, subst_terms)
})
}
/* sort algebra */
sealed case class Classrel(class1: String, class2: String, prop: Prop) {
def cache(cache: Term.Cache): Classrel =
Classrel(cache.string(class1), cache.string(class2), prop.cache(cache))
}
def read_classrel(theory_context: Export.Theory_Context): List[Classrel] = {
val body = theory_context.uncompressed_yxml(Export.THEORY_PREFIX + "classrel")
val classrel = {
import XML.Decode._
list(pair(decode_prop, pair(string, string)))(body)
}
for ((prop, (c1, c2)) <- classrel) yield Classrel(c1, c2, prop)
}
sealed case class Arity(
type_name: String,
domain: List[Term.Sort],
codomain: String,
prop: Prop
) {
def cache(cache: Term.Cache): Arity =
Arity(cache.string(type_name), domain.map(cache.sort), cache.string(codomain),
prop.cache(cache))
}
def read_arities(theory_context: Export.Theory_Context): List[Arity] = {
val body = theory_context.uncompressed_yxml(Export.THEORY_PREFIX + "arities")
val arities = {
import XML.Decode._
import Term_XML.Decode._
list(pair(decode_prop, triple(string, list(sort), string)))(body)
}
for ((prop, (a, b, c)) <- arities) yield Arity(a, b, c, prop)
}
/* Pure constdefs */
sealed case class Constdef(name: String, axiom_name: String) {
def cache(cache: Term.Cache): Constdef =
Constdef(cache.string(name), cache.string(axiom_name))
}
def read_constdefs(theory_context: Export.Theory_Context): List[Constdef] = {
val body = theory_context.uncompressed_yxml(Export.THEORY_PREFIX + "constdefs")
val constdefs = {
import XML.Decode._
list(pair(string, string))(body)
}
for ((name, axiom_name) <- constdefs) yield Constdef(name, axiom_name)
}
/* HOL typedefs */
sealed case class Typedef(
name: String,
rep_type: Term.Typ,
abs_type: Term.Typ,
rep_name: String,
abs_name: String,
axiom_name: String
) {
def cache(cache: Term.Cache): Typedef =
Typedef(cache.string(name),
cache.typ(rep_type),
cache.typ(abs_type),
cache.string(rep_name),
cache.string(abs_name),
cache.string(axiom_name))
}
def read_typedefs(theory_context: Export.Theory_Context): List[Typedef] = {
val body = theory_context.uncompressed_yxml(Export.THEORY_PREFIX + "typedefs")
val typedefs = {
import XML.Decode._
import Term_XML.Decode._
list(pair(string, pair(typ, pair(typ, pair(string, pair(string, string))))))(body)
}
for { (name, (rep_type, (abs_type, (rep_name, (abs_name, axiom_name))))) <- typedefs }
yield Typedef(name, rep_type, abs_type, rep_name, abs_name, axiom_name)
}
/* HOL datatypes */
sealed case class Datatype(
pos: Position.T,
name: String,
co: Boolean,
typargs: List[(String, Term.Sort)],
typ: Term.Typ,
constructors: List[(Term.Term, Term.Typ)]
) {
def id: Option[Long] = Position.Id.unapply(pos)
def cache(cache: Term.Cache): Datatype =
Datatype(
cache.position(pos),
cache.string(name),
co,
typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
cache.typ(typ),
constructors.map({ case (term, typ) => (cache.term(term), cache.typ(typ)) }))
}
def read_datatypes(theory_context: Export.Theory_Context): List[Datatype] = {
val body = theory_context.uncompressed_yxml(Export.THEORY_PREFIX + "datatypes")
val datatypes = {
import XML.Decode._
import Term_XML.Decode._
list(pair(properties, pair(string, pair(bool, pair(list(pair(string, sort)),
pair(typ, list(pair(term, typ))))))))(body)
}
for ((pos, (name, (co, (typargs, (typ, constructors))))) <- datatypes)
yield Datatype(pos, name, co, typargs, typ, constructors)
}
/* Pure spec rules */
sealed abstract class Recursion {
def cache(cache: Term.Cache): Recursion =
this match {
case Primrec(types) => Primrec(types.map(cache.string))
case Primcorec(types) => Primcorec(types.map(cache.string))
case _ => this
}
}
case class Primrec(types: List[String]) extends Recursion
case object Recdef extends Recursion
case class Primcorec(types: List[String]) extends Recursion
case object Corec extends Recursion
case object Unknown_Recursion extends Recursion
val decode_recursion: XML.Decode.T[Recursion] = {
import XML.Decode._
variant(List(
{ case (Nil, a) => Primrec(list(string)(a)) },
{ case (Nil, Nil) => Recdef },
{ case (Nil, a) => Primcorec(list(string)(a)) },
{ case (Nil, Nil) => Corec },
{ case (Nil, Nil) => Unknown_Recursion }))
}
sealed abstract class Rough_Classification {
def is_equational: Boolean = this.isInstanceOf[Equational]
def is_inductive: Boolean = this == Inductive
def is_co_inductive: Boolean = this == Co_Inductive
def is_relational: Boolean = is_inductive || is_co_inductive
def is_unknown: Boolean = this == Unknown
def cache(cache: Term.Cache): Rough_Classification =
this match {
case Equational(recursion) => Equational(recursion.cache(cache))
case _ => this
}
}
case class Equational(recursion: Recursion) extends Rough_Classification
case object Inductive extends Rough_Classification
case object Co_Inductive extends Rough_Classification
case object Unknown extends Rough_Classification
val decode_rough_classification: XML.Decode.T[Rough_Classification] = {
import XML.Decode._
variant(List(
{ case (Nil, a) => Equational(decode_recursion(a)) },
{ case (Nil, Nil) => Inductive },
{ case (Nil, Nil) => Co_Inductive },
{ case (Nil, Nil) => Unknown }))
}
sealed case class Spec_Rule(
pos: Position.T,
name: String,
rough_classification: Rough_Classification,
typargs: List[(String, Term.Sort)],
args: List[(String, Term.Typ)],
terms: List[(Term.Term, Term.Typ)],
rules: List[Term.Term]
) {
def id: Option[Long] = Position.Id.unapply(pos)
def cache(cache: Term.Cache): Spec_Rule =
Spec_Rule(
cache.position(pos),
cache.string(name),
rough_classification.cache(cache),
typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
terms.map({ case (term, typ) => (cache.term(term), cache.typ(typ)) }),
rules.map(cache.term))
}
def read_spec_rules(theory_context: Export.Theory_Context): List[Spec_Rule] = {
val body = theory_context.uncompressed_yxml(Export.THEORY_PREFIX + "spec_rules")
val spec_rules = {
import XML.Decode._
import Term_XML.Decode._
list(
pair(properties, pair(string, pair(decode_rough_classification,
pair(list(pair(string, sort)), pair(list(pair(string, typ)),
pair(list(pair(term, typ)), list(term))))))))(body)
}
for ((pos, (name, (rough_classification, (typargs, (args, (terms, rules)))))) <- spec_rules)
yield Spec_Rule(pos, name, rough_classification, typargs, args, terms, rules)
}
/* other entities */
sealed case class Other() extends Content[Other] {
override def cache(cache: Term.Cache): Other = this
}
def read_others(theory_context: Export.Theory_Context): Map[String, List[Entity[Other]]] = {
val kinds =
theory_context.get(Export.THEORY_PREFIX + "other_kinds") match {
case Some(entry) => split_lines(entry.uncompressed.text)
case None => Nil
}
val other = Other()
def read_other(kind: String): List[Entity[Other]] =
read_entities(theory_context, Export.THEORY_PREFIX + "other/" + kind, kind, _ => other)
kinds.map(kind => kind -> read_other(kind)).toMap
}
}
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,670 +1,669 @@
/* Title: Pure/Thy/presentation.scala
Author: Makarius
HTML presentation of PIDE document content.
*/
package isabelle
import scala.annotation.tailrec
import scala.collection.immutable.SortedMap
import scala.collection.mutable
object Presentation {
/** HTML documents **/
/* HTML context */
sealed case class HTML_Document(title: String, content: String)
abstract class HTML_Context {
/* directory structure and resources */
def nodes: Nodes
def root_dir: Path
def theory_session(name: Document.Node.Name): Sessions.Info
def session_dir(info: Sessions.Info): Path =
root_dir + Path.explode(info.chapter_session)
def theory_dir(name: Document.Node.Name): Path =
session_dir(theory_session(name))
def files_path(name: Document.Node.Name, path: Path): Path =
theory_dir(name) + Path.explode("files") + path.squash.html
/* HTML content */
def head(title: String, rest: XML.Body = Nil): XML.Tree =
HTML.div("head", HTML.chapter(title) :: rest)
def source(body: XML.Body): XML.Tree = HTML.pre("source", body)
def contents(
heading: String,
items: List[XML.Body],
css_class: String = "contents"
) : List[XML.Elem] = {
if (items.isEmpty) Nil
else List(HTML.div(css_class, List(HTML.section(heading), HTML.itemize(items))))
}
val isabelle_css: String = File.read(HTML.isabelle_css)
def html_document(title: String, body: XML.Body, fonts_css: String): HTML_Document = {
val content =
HTML.output_document(
List(
HTML.style(fonts_css + "\n\n" + isabelle_css),
HTML.title(title)),
List(HTML.source(body)), css = "", structural = false)
HTML_Document(title, content)
}
}
/* presentation elements */
sealed case class Elements(
html: Markup.Elements = Markup.Elements.empty,
entity: Markup.Elements = Markup.Elements.empty,
language: Markup.Elements = Markup.Elements.empty)
val elements1: Elements =
Elements(
html = Rendering.foreground_elements ++ Rendering.text_color_elements +
Markup.NUMERAL + Markup.COMMENT + Markup.ENTITY + Markup.LANGUAGE,
entity = Markup.Elements(Markup.THEORY, Markup.TYPE_NAME, Markup.CONSTANT, Markup.FACT,
Markup.CLASS, Markup.LOCALE, Markup.FREE))
val elements2: Elements =
Elements(
html = elements1.html ++ Rendering.markdown_elements,
language = Markup.Elements(Markup.Language.DOCUMENT))
/* per-session node info */
sealed case class File_Info(theory: String, is_theory: Boolean = false)
object Node_Info {
val empty: Node_Info = new Node_Info(Map.empty, Map.empty, Nil)
def make(theory: Export_Theory.Theory): Node_Info = {
val by_range = theory.entity_iterator.toList.groupBy(_.range)
val by_kind_name =
theory.entity_iterator.map(entity => ((entity.kind, entity.name), entity)).toMap
val others = theory.others.keySet.toList
new Node_Info(by_range, by_kind_name, others)
}
}
class Node_Info private(
by_range: Map[Symbol.Range, List[Export_Theory.Entity0]],
by_kind_name: Map[(String, String), Export_Theory.Entity0],
val others: List[String]) {
def for_range(range: Symbol.Range): List[Export_Theory.Entity0] =
by_range.getOrElse(range, Nil)
def get_kind_name(kind: String, name: String): Option[String] =
by_kind_name.get((kind, name)).map(_.kname)
}
object Nodes {
val empty: Nodes = new Nodes(Map.empty, Map.empty)
def read(
database_context: Export.Database_Context,
deps: Sessions.Deps,
presentation_sessions: List[String]
): Nodes = {
def open_session(session: String): Export.Session_Context =
database_context.open_session(deps.base_info(session))
type Batch = (String, List[String])
val batches =
presentation_sessions.foldLeft((Set.empty[String], List.empty[Batch]))(
{ case ((seen, batches), session) =>
val thys = deps(session).loaded_theories.keys.filterNot(seen)
(seen ++ thys, (session, thys) :: batches)
})._2
val theory_node_info =
Par_List.map[Batch, List[(String, Node_Info)]](
{ case (session, thys) =>
using(open_session(session)) { session_context =>
for (thy_name <- thys) yield {
- val theory_context = session_context.theory(thy_name)
- val theory =
- Export_Theory.read_theory(theory_context,
- permissive = true, cache = session_context.cache)
+ val theory_context =
+ session_context.theory(thy_name, other_cache = Some(Term.Cache.none))
+ val theory = Export_Theory.read_theory(theory_context, permissive = true)
thy_name -> Node_Info.make(theory)
}
}
}, batches).flatten.toMap
val files_info =
deps.sessions_structure.build_requirements(presentation_sessions).flatMap(session =>
using(open_session(session)) { session_context =>
session_context.theory_names().flatMap { theory =>
session_context.theory(theory).files() match {
case None => Nil
case Some((thy, blobs)) =>
val thy_file_info = File_Info(theory, is_theory = true)
(thy -> thy_file_info) :: blobs.map(_ -> File_Info(theory))
}
}
}).toMap
new Nodes(theory_node_info, files_info)
}
}
class Nodes private(
theory_node_info: Map[String, Node_Info],
val files_info: Map[String, File_Info]
) {
def apply(name: String): Node_Info = theory_node_info.getOrElse(name, Node_Info.empty)
def get(name: String): Option[Node_Info] = theory_node_info.get(name)
}
/* formal entities */
type Entity = Export_Theory.Entity[Export_Theory.No_Content]
object Entity_Context {
object Theory_Ref {
def unapply(props: Properties.T): Option[Document.Node.Name] =
(props, props, props) match {
case (Markup.Kind(Markup.THEORY), Markup.Name(theory), Position.Def_File(thy_file)) =>
Some(Resources.file_node(Path.explode(thy_file), theory = theory))
case _ => None
}
}
object Entity_Ref {
def unapply(props: Properties.T): Option[(Path, Option[String], String, String)] =
(props, props, props, props) match {
case (Markup.Entity.Ref.Prop(_), Position.Def_File(def_file),
Markup.Kind(kind), Markup.Name(name)) =>
val def_theory = Position.Def_Theory.unapply(props)
Some((Path.explode(def_file), def_theory, kind, name))
case _ => None
}
}
val empty: Entity_Context = new Entity_Context
def make(
session: String,
deps: Sessions.Deps,
node: Document.Node.Name,
html_context: HTML_Context): Entity_Context =
new Entity_Context {
private val seen_ranges: mutable.Set[Symbol.Range] = mutable.Set.empty
override def make_def(range: Symbol.Range, body: XML.Body): Option[XML.Elem] = {
body match {
case List(XML.Elem(Markup("span", List("id" -> _)), _)) => None
case _ =>
Some {
val entities = html_context.nodes(node.theory).for_range(range)
val body1 =
if (seen_ranges.contains(range)) {
HTML.entity_def(HTML.span(HTML.id(offset_id(range)), body))
}
else HTML.span(body)
entities.map(_.kname).foldLeft(body1) {
case (elem, id) => HTML.entity_def(HTML.span(HTML.id(id), List(elem)))
}
}
}
}
private def offset_id(range: Text.Range): String =
"offset_" + range.start + ".." + range.stop
private def physical_ref(thy_name: String, props: Properties.T): Option[String] = {
for {
range <- Position.Def_Range.unapply(props)
if thy_name == node.theory
} yield {
seen_ranges += range
offset_id(range)
}
}
private def logical_ref(thy_name: String, kind: String, name: String): Option[String] =
html_context.nodes.get(thy_name).flatMap(_.get_kind_name(kind, name))
override def make_ref(props: Properties.T, body: XML.Body): Option[XML.Elem] = {
props match {
case Theory_Ref(node_name) =>
node_relative(deps, session, node_name).map(html_dir =>
HTML.link(html_dir + html_name(node_name), body))
case Entity_Ref(file_path, def_theory, kind, name) if file_path.get_ext == "thy" =>
for {
thy_name <-
def_theory orElse (if (File.eq(node.path, file_path)) Some(node.theory) else None)
node_name = Resources.file_node(file_path, theory = thy_name)
html_dir <- node_relative(deps, session, node_name)
html_file = node_file(node_name)
html_ref <-
logical_ref(thy_name, kind, name) orElse physical_ref(thy_name, props)
} yield {
HTML.entity_ref(HTML.link(html_dir + html_file + "#" + html_ref, body))
}
case _ => None
}
}
}
}
class Entity_Context {
def make_def(range: Symbol.Range, body: XML.Body): Option[XML.Elem] = None
def make_ref(props: Properties.T, body: XML.Body): Option[XML.Elem] = None
}
/* HTML output */
private val div_elements =
Set(HTML.div.name, HTML.pre.name, HTML.par.name, HTML.list.name, HTML.`enum`.name,
HTML.descr.name)
def make_html(
entity_context: Entity_Context,
elements: Elements,
xml: XML.Body
): XML.Body = {
def html_div(html: XML.Body): Boolean =
html exists {
case XML.Elem(markup, body) => div_elements.contains(markup.name) || html_div(body)
case XML.Text(_) => false
}
def html_class(c: String, html: XML.Body): XML.Body =
if (c == "") html
else if (html_div(html)) List(HTML.div(c, html))
else List(HTML.span(c, html))
def html_body(xml_body: XML.Body, end_offset: Symbol.Offset): (XML.Body, Symbol.Offset) =
xml_body.foldRight((List.empty[XML.Tree], end_offset)) { case (tree, (res, end_offset1)) =>
val (res1, offset) = html_body_single(tree, end_offset1)
(res1 ++ res, offset)
}
@tailrec
def html_body_single(xml_tree: XML.Tree, end_offset: Symbol.Offset): (XML.Body, Symbol.Offset) =
xml_tree match {
case XML.Wrapped_Elem(markup, _, body) => html_body_single(XML.Elem(markup, body), end_offset)
case XML.Elem(Markup(Markup.ENTITY, props @ Markup.Kind(kind)), body) =>
val (body1, offset) = html_body(body, end_offset)
if (elements.entity(kind)) {
entity_context.make_ref(props, body1) match {
case Some(link) => (List(link), offset)
case None => (body1, offset)
}
}
else (body1, offset)
case XML.Elem(Markup(Markup.LANGUAGE, Markup.Name(name)), body) =>
val (body1, offset) = html_body(body, end_offset)
(html_class(if (elements.language(name)) name else "", body1), offset)
case XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), body) =>
val (body1, offset) = html_body(body, end_offset)
(List(HTML.par(body1)), offset)
case XML.Elem(Markup(Markup.MARKDOWN_ITEM, _), body) =>
val (body1, offset) = html_body(body, end_offset)
(List(HTML.item(body1)), offset)
case XML.Elem(Markup(Markup.Markdown_Bullet.name, _), text) =>
(Nil, end_offset - XML.symbol_length(text))
case XML.Elem(Markup.Markdown_List(kind), body) =>
val (body1, offset) = html_body(body, end_offset)
if (kind == Markup.ENUMERATE) (List(HTML.`enum`(body1)), offset)
else (List(HTML.list(body1)), offset)
case XML.Elem(markup, body) =>
val name = markup.name
val (body1, offset) = html_body(body, end_offset)
val html =
markup.properties match {
case Markup.Kind(kind) if kind == Markup.COMMAND || kind == Markup.KEYWORD =>
html_class(kind, body1)
case _ =>
body1
}
Rendering.foreground.get(name) orElse Rendering.text_color.get(name) match {
case Some(c) => (html_class(c.toString, html), offset)
case None => (html_class(name, html), offset)
}
case XML.Text(text) =>
val offset = end_offset - Symbol.length(text)
val body = HTML.text(Symbol.decode(text))
entity_context.make_def(Text.Range(offset, end_offset), body) match {
case Some(body1) => (List(body1), offset)
case None => (body, offset)
}
}
html_body(xml, XML.symbol_length(xml) + 1)._1
}
/* PIDE HTML document */
def html_document(
snapshot: Document.Snapshot,
html_context: HTML_Context,
elements: Elements,
plain_text: Boolean = false,
fonts_css: String = HTML.fonts_css()
): HTML_Document = {
require(!snapshot.is_outdated, "document snapshot outdated")
val name = snapshot.node_name
if (plain_text) {
val title = "File " + Symbol.cartouche_decoded(name.path.file_name)
val body = HTML.text(snapshot.node.source)
html_context.html_document(title, body, fonts_css)
}
else {
Resources.html_document(snapshot) getOrElse {
val title =
if (name.is_theory) "Theory " + quote(name.theory_base_name)
else "File " + Symbol.cartouche_decoded(name.path.file_name)
val xml = snapshot.xml_markup(elements = elements.html)
val body = make_html(Entity_Context.empty, elements, xml)
html_context.html_document(title, body, fonts_css)
}
}
}
/** HTML presentation **/
/* 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)
}
/* 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
}
def update_chapter(
presentation_dir: Path,
chapter: String,
new_sessions: List[(String, String)]
): Unit = {
val dir = Isabelle_System.make_directory(presentation_dir + Path.basic(chapter))
val sessions0 =
try { read_sessions(dir) }
catch { case _: XML.Error => Nil }
val sessions = (SortedMap.empty[String, String] ++ sessions0 ++ new_sessions).toList
File.write(dir + sessions_path,
{
import XML.Encode._
YXML.string_of_body(list(pair(string, string))(sessions))
})
val title = "Isabelle/" + chapter + " sessions"
HTML.write_document(dir, "index.html",
List(HTML.title(title + Isabelle_System.isabelle_heading())),
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)))) })))))),
base = Some(presentation_dir))
}
def update_root(presentation_dir: Path): Unit = {
Isabelle_System.make_directory(presentation_dir)
HTML.init_fonts(presentation_dir)
Isabelle_System.copy_file(Path.explode("~~/lib/logo/isabelle.gif"),
presentation_dir + Path.explode("isabelle.gif"))
val title = "The " + XML.text(Isabelle_System.isabelle_name()) + " Library"
File.write(presentation_dir + Path.explode("index.html"),
HTML.header +
"""
""" + HTML.head_meta + """
""" + title + """
""" + File.read(Path.explode("~~/lib/html/library_index_content.template")) +
"""
""" + HTML.footer)
}
/* present session */
val session_graph_path = Path.explode("session_graph.pdf")
val readme_path = Path.explode("README.html")
def html_name(name: Document.Node.Name): String = Path.explode(name.theory_base_name).html.implode
def files_path(src_path: Path): String = (Path.explode("files") + src_path.squash.html).implode
private def node_file(name: Document.Node.Name): String =
if (name.node.endsWith(".thy")) html_name(name) else files_path(name.path)
private def session_relative(
deps: Sessions.Deps,
session0: String,
session1: String
): Option[String] = {
for {
info0 <- deps.sessions_structure.get(session0)
info1 <- deps.sessions_structure.get(session1)
} yield info0.relative_path(info1)
}
def node_relative(
deps: Sessions.Deps,
session0: String,
node_name: Document.Node.Name
): Option[String] = {
val session1 = deps(session0).theory_qualifier(node_name)
session_relative(deps, session0, session1)
}
def session_html(
session_context: Export.Session_Context,
deps: Sessions.Deps,
progress: Progress = new Progress,
verbose: Boolean = false,
html_context: HTML_Context,
session_elements: Elements
): Unit = {
val session = session_context.session_name
val info = session_context.sessions_structure(session)
val options = info.options
val base = session_context.session_base
val session_dir = Isabelle_System.make_directory(html_context.session_dir(info))
Bytes.write(session_dir + session_graph_path,
graphview.Graph_File.make_pdf(options, base.session_graph_display))
val documents =
for {
doc <- info.document_variants
db <- session_context.session_db()
document <- Document_Build.read_document(db, session, doc.name)
} yield {
val doc_path = (session_dir + doc.path.pdf).expand
if (verbose) progress.echo("Presenting document " + session + "/" + doc.name)
if (options.bool("document_echo")) progress.echo("Document at " + doc_path)
Bytes.write(doc_path, document.pdf)
doc
}
val view_links = {
val deps_link =
HTML.link(session_graph_path, HTML.text("theory dependencies"))
val readme_links =
if ((info.dir + readme_path).is_file) {
Isabelle_System.copy_file(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 entity_context(name: Document.Node.Name): Entity_Context =
Entity_Context.make(session, deps, name, html_context)
sealed case class Seen_File(
src_path: Path,
thy_name: Document.Node.Name,
thy_session: String
) {
val files_path: Path = html_context.files_path(thy_name, src_path)
def check(src_path1: Path, thy_name1: Document.Node.Name, thy_session1: String): Boolean = {
val files_path1 = html_context.files_path(thy_name1, src_path1)
(src_path == src_path1 || files_path == files_path1) && thy_session == thy_session1
}
}
var seen_files = List.empty[Seen_File]
def present_theory(name: Document.Node.Name): Option[XML.Body] = {
progress.expose_interrupt()
Build_Job.read_theory(session_context.theory(name.theory)).flatMap { command =>
if (verbose) progress.echo("Presenting theory " + name)
val snapshot = Document.State.init.snippet(command)
val thy_elements =
session_elements.copy(entity =
html_context.nodes(name.theory).others.foldLeft(session_elements.entity)(_ + _))
val files_html =
for {
(src_path, xml) <- snapshot.xml_markup_blobs(elements = thy_elements.html)
if xml.nonEmpty
}
yield {
progress.expose_interrupt()
if (verbose) progress.echo("Presenting file " + src_path)
(src_path, html_context.source(
make_html(Entity_Context.empty, thy_elements, xml)))
}
val thy_html =
html_context.source(
make_html(entity_context(name), thy_elements,
snapshot.xml_markup(elements = thy_elements.html)))
val thy_session = html_context.theory_session(name).name
val thy_dir = Isabelle_System.make_directory(html_context.theory_dir(name))
val files =
for { (src_path, file_html) <- files_html }
yield {
seen_files.find(_.check(src_path, name, thy_session)) match {
case None => seen_files ::= Seen_File(src_path, name, thy_session)
case Some(seen_file) =>
error("Incoherent use of file name " + src_path + " as " + files_path(src_path) +
" in theory " + seen_file.thy_name + " vs. " + name)
}
val file_path = html_context.files_path(name, src_path)
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), file_html),
base = Some(html_context.root_dir))
List(HTML.link(files_path(src_path), HTML.text(file_title)))
}
val thy_title = "Theory " + name.theory_base_name
HTML.write_document(thy_dir, html_name(name),
List(HTML.title(thy_title)), List(html_context.head(thy_title), thy_html),
base = Some(html_context.root_dir))
if (thy_session == session) {
Some(
List(HTML.link(html_name(name),
HTML.text(name.theory_base_name) :::
(if (files.isEmpty) Nil else List(HTML.itemize(files))))))
}
else None
}
}
val theories = base.proper_session_theories.flatMap(present_theory)
val title = "Session " + session
HTML.write_document(session_dir, "index.html",
List(HTML.title(title + Isabelle_System.isabelle_heading())),
html_context.head(title, List(HTML.par(view_links))) ::
html_context.contents("Theories", theories),
base = Some(html_context.root_dir))
}
}