1/*  Title:      Pure/Tools/doc.scala
2    Author:     Makarius
3
4Access to Isabelle documentation.
5*/
6
7package isabelle
8
9
10import scala.util.matching.Regex
11
12
13object Doc
14{
15  /* dirs */
16
17  def dirs(): List[Path] =
18    Path.split(Isabelle_System.getenv("ISABELLE_DOCS"))
19
20
21  /* contents */
22
23  private def contents_lines(): List[(Path, String)] =
24    for {
25      dir <- dirs()
26      catalog = dir + Path.basic("Contents")
27      if catalog.is_file
28      line <- split_lines(Library.trim_line(File.read(catalog)))
29    } yield (dir, line)
30
31  sealed abstract class Entry
32  case class Section(text: String, important: Boolean) extends Entry
33  case class Doc(name: String, title: String, path: Path) extends Entry
34  case class Text_File(name: String, path: Path) extends Entry
35
36  def text_file(name: Path): Option[Text_File] =
37  {
38    val path = Path.variable("ISABELLE_HOME") + name
39    if (path.is_file) Some(Text_File(name.implode, path))
40    else None
41  }
42
43  private val Section_Entry = new Regex("""^(\S.*)\s*$""")
44  private val Doc_Entry = new Regex("""^\s+(\S+)\s+(.+)\s*$""")
45
46  private def release_notes(): List[Entry] =
47    Section("Release notes", true) ::
48      Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_RELEASE_NOTES")).flatMap(text_file(_))
49
50  private def examples(): List[Entry] =
51    Section("Examples", true) ::
52      Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_EXAMPLES")).map(file =>
53        text_file(file) match {
54          case Some(entry) => entry
55          case None => error("Bad entry in ISABELLE_DOCS_EXAMPLES: " + file)
56        })
57
58  def contents(): List[Entry] =
59  {
60    val main_contents =
61      for {
62        (dir, line) <- contents_lines()
63        entry <-
64          line match {
65            case Section_Entry(text) =>
66              Library.try_unsuffix("!", text) match {
67                case None => Some(Section(text, false))
68                case Some(txt) => Some(Section(txt, true))
69              }
70            case Doc_Entry(name, title) => Some(Doc(name, title, dir + Path.basic(name)))
71            case _ => None
72          }
73      } yield entry
74
75    examples() ::: release_notes() ::: main_contents
76  }
77
78  def doc_names(): List[String] =
79    for (Doc(name, _, _) <- contents()) yield name
80
81
82  /* view */
83
84  def view(path: Path)
85  {
86    if (path.is_file) Output.writeln(Library.trim_line(File.read(path)), stdout = true)
87    else {
88      val pdf = path.ext("pdf")
89      if (pdf.is_file) Isabelle_System.pdf_viewer(pdf)
90      else error("Bad Isabelle documentation file: " + pdf)
91    }
92  }
93
94
95  /* Isabelle tool wrapper */
96
97  val isabelle_tool = Isabelle_Tool("doc", "view Isabelle documentation", args =>
98  {
99    val getopts = Getopts("""
100Usage: isabelle doc [DOC ...]
101
102  View Isabelle documentation.
103""")
104    val docs = getopts(args)
105
106    val entries = contents()
107    if (docs.isEmpty) Output.writeln(cat_lines(contents_lines().map(_._2)), stdout = true)
108    else {
109      docs.foreach(doc =>
110        entries.collectFirst { case Doc(name, _, path) if doc == name => path } match {
111          case Some(path) => view(path)
112          case None => error("No Isabelle documentation entry: " + quote(doc))
113        }
114      )
115    }
116  })
117}
118