/* Title: Pure/Tools/doc.scala
Author: Makarius
Access to Isabelle examples and documentation.
*/
package isabelle
import scala.collection.mutable
object Doc {
/* entries */
case class Section(title: String, important: Boolean, entries: List[Entry])
case class Entry(name: String, path: Path, title: String = "") {
def view(): Unit = Doc.view(path)
override def toString: String = // GUI label
if (title.nonEmpty) {
"<html><b>" + HTML.output(name) + "</b>: " + HTML.output(title) + "</html>"
}
else name
}
def plain_file(path: Path): Option[Entry] =
if (path.is_file && !path.is_pdf) {
val a = path.implode
val b = Library.try_unprefix("$ISABELLE_HOME/", a).getOrElse(a)
Some(Entry(b, path))
}
else None
/* contents */
def dirs(): List[Path] =
Path.split(Isabelle_System.getenv("ISABELLE_DOCS"))
private def contents_lines(): List[(Path, String)] =
for {
dir <- dirs()
catalog = dir + Path.basic("Contents")
if catalog.is_file
line <- Library.trim_split_lines(File.read(catalog))
} yield (dir, line)
object Contents {
def apply(sections: List[Section]): Contents = new Contents(sections)
def section(title: String, important: Boolean, entries: List[Entry]): Contents =
apply(List(Section(title, important, entries)))
}
class Contents private(val sections: List[Section]) {
def ++ (other: Contents): Contents = new Contents(sections ::: other.sections)
def entries(name: String => Boolean = _ => true, pdf: Boolean = false): List[Entry] =
sections.flatMap(s => s.entries.filter(e => name(e.name) && (!pdf || e.path.is_pdf)))
}
def release_notes(): Contents =
Contents.section("Release Notes", true,
Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_RELEASE_NOTES")).flatMap(plain_file))
def examples(): Contents =
Contents.section("Examples", true,
Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_EXAMPLES")).map(file =>
plain_file(file) match {
case Some(entry) => entry
case None => error("Bad entry in ISABELLE_DOCS_EXAMPLES: " + file)
}))
def main_contents(): Contents = {
val result = new mutable.ListBuffer[Section]
val entries = new mutable.ListBuffer[Entry]
var section: Option[Section] = None
def flush(): Unit =
if (section.nonEmpty) {
result += section.get.copy(entries = entries.toList)
entries.clear()
section = None
}
def begin(s: Section): Unit = {
flush()
section = Some(s)
}
val Section_ = """^(\S.*)\s*$""".r
val Entry_ = """^\s+(\S+)\s+(.+)\s*$""".r
for ((dir, line) <- contents_lines()) {
line match {
case Section_(text) =>
Library.try_unsuffix("!", text) match {
case None => begin(Section(text, false, Nil))
case Some(txt) => begin(Section(txt, true, Nil))
}
case Entry_(name, title) =>
val path = dir + Path.basic(name)
entries += Entry(name, if (path.is_file) path else path.pdf, title = title)
case _ =>
}
}
flush()
Contents(result.toList)
}
def contents(): Contents = {
examples() ++ release_notes() ++ main_contents()
}
object Doc_Names extends Scala.Fun_String("doc_names") {
val here = Scala_Project.here
def apply(arg: String): String =
if (arg.nonEmpty) error("Bad argument: " + quote(arg))
else cat_lines((for (entry <- contents().entries(pdf = true)) yield entry.name).sorted)
}
/* view */
def view(path: Path): Unit = {
if (!path.is_file) error("Bad Isabelle documentation file: " + path)
else if (path.is_pdf) Isabelle_System.pdf_viewer(path)
else Output.writeln(Library.trim_line(File.read(path)), stdout = true)
}
/* Isabelle tool wrapper */
val isabelle_tool = Isabelle_Tool("doc", "view Isabelle documentation",
Scala_Project.here,
{ args =>
val getopts = Getopts("""
Usage: isabelle doc [DOC ...]
View Isabelle documentation.
""")
val docs = getopts(args)
if (docs.isEmpty) Output.writeln(cat_lines(contents_lines().map(_._2)), stdout = true)
else {
docs.foreach(name =>
contents().entries(name = docs.contains).headOption match {
case Some(entry) => entry.view()
case None => error("No Isabelle documentation entry: " + quote(name))
}
)
}
})
}