src/Pure/Tools/doc.scala
author wenzelm
Sun, 03 Apr 2016 22:31:16 +0200
changeset 62831 5560905a32ae
parent 62454 38c89353b349
child 67178 70576478bda9
permissions -rw-r--r--
prefer internal tool;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
52444
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52429
diff changeset
     1
/*  Title:      Pure/Tools/doc.scala
52427
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
     3
56424
7032378cc097 proper settings instead of hard-wired information;
wenzelm
parents: 56423
diff changeset
     4
Access to Isabelle documentation.
52427
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
     5
*/
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
     6
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
     7
package isabelle
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
     8
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
     9
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    10
import scala.util.matching.Regex
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    11
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    12
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    13
object Doc
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    14
{
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    15
  /* dirs */
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    16
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    17
  def dirs(): List[Path] =
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    18
    Path.split(Isabelle_System.getenv("ISABELLE_DOCS")).map(dir =>
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    19
      if (dir.is_dir) dir
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    20
      else error("Bad documentation directory: " + dir))
52740
bceec99254b0 documentation is always in PDF;
wenzelm
parents: 52542
diff changeset
    21
52427
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    22
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    23
  /* contents */
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    24
56422
7490555d7dff clarified Doc entry: more explicit path;
wenzelm
parents: 56276
diff changeset
    25
  private def contents_lines(): List[(Path, String)] =
52444
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52429
diff changeset
    26
    for {
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52429
diff changeset
    27
      dir <- dirs()
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52429
diff changeset
    28
      catalog = dir + Path.basic("Contents")
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52429
diff changeset
    29
      if catalog.is_file
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52429
diff changeset
    30
      line <- split_lines(Library.trim_line(File.read(catalog)))
56422
7490555d7dff clarified Doc entry: more explicit path;
wenzelm
parents: 56276
diff changeset
    31
    } yield (dir, line)
52444
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52429
diff changeset
    32
52427
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    33
  sealed abstract class Entry
56423
c2f52824dbb2 explicit indication of important doc sections ("!"), which are expanded in the tree view;
wenzelm
parents: 56422
diff changeset
    34
  case class Section(text: String, important: Boolean) extends Entry
56422
7490555d7dff clarified Doc entry: more explicit path;
wenzelm
parents: 56276
diff changeset
    35
  case class Doc(name: String, title: String, path: Path) extends Entry
52542
19d674acb764 more release notes according to availability in proper release vs. repository clone;
wenzelm
parents: 52541
diff changeset
    36
  case class Text_File(name: String, path: Path) extends Entry
52427
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    37
56424
7032378cc097 proper settings instead of hard-wired information;
wenzelm
parents: 56423
diff changeset
    38
  def text_file(name: Path): Option[Text_File] =
53777
06a6216f733e immediate access to some elementary examples;
wenzelm
parents: 52740
diff changeset
    39
  {
56424
7032378cc097 proper settings instead of hard-wired information;
wenzelm
parents: 56423
diff changeset
    40
    val path = Path.variable("ISABELLE_HOME") + name
7032378cc097 proper settings instead of hard-wired information;
wenzelm
parents: 56423
diff changeset
    41
    if (path.is_file) Some(Text_File(name.implode, path))
53777
06a6216f733e immediate access to some elementary examples;
wenzelm
parents: 52740
diff changeset
    42
    else None
06a6216f733e immediate access to some elementary examples;
wenzelm
parents: 52740
diff changeset
    43
  }
06a6216f733e immediate access to some elementary examples;
wenzelm
parents: 52740
diff changeset
    44
52444
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52429
diff changeset
    45
  private val Section_Entry = new Regex("""^(\S.*)\s*$""")
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52429
diff changeset
    46
  private val Doc_Entry = new Regex("""^\s+(\S+)\s+(.+)\s*$""")
52427
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    47
52542
19d674acb764 more release notes according to availability in proper release vs. repository clone;
wenzelm
parents: 52541
diff changeset
    48
  private def release_notes(): List[Entry] =
56423
c2f52824dbb2 explicit indication of important doc sections ("!"), which are expanded in the tree view;
wenzelm
parents: 56422
diff changeset
    49
    Section("Release notes", true) ::
56424
7032378cc097 proper settings instead of hard-wired information;
wenzelm
parents: 56423
diff changeset
    50
      Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_RELEASE_NOTES")).flatMap(text_file(_))
52541
97c950217d7f quick access to release notes (imitating website/documentation.html);
wenzelm
parents: 52448
diff changeset
    51
53777
06a6216f733e immediate access to some elementary examples;
wenzelm
parents: 52740
diff changeset
    52
  private def examples(): List[Entry] =
56424
7032378cc097 proper settings instead of hard-wired information;
wenzelm
parents: 56423
diff changeset
    53
    Section("Examples", true) ::
7032378cc097 proper settings instead of hard-wired information;
wenzelm
parents: 56423
diff changeset
    54
      Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_EXAMPLES")).map(file =>
7032378cc097 proper settings instead of hard-wired information;
wenzelm
parents: 56423
diff changeset
    55
        text_file(file) match {
7032378cc097 proper settings instead of hard-wired information;
wenzelm
parents: 56423
diff changeset
    56
          case Some(entry) => entry
56425
d12653fbd5b1 tuned error;
wenzelm
parents: 56424
diff changeset
    57
          case None => error("Bad entry in ISABELLE_DOCS_EXAMPLES: " + file)
56424
7032378cc097 proper settings instead of hard-wired information;
wenzelm
parents: 56423
diff changeset
    58
        })
53777
06a6216f733e immediate access to some elementary examples;
wenzelm
parents: 52740
diff changeset
    59
52444
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52429
diff changeset
    60
  def contents(): List[Entry] =
61157
13f4056c42d7 clarified order;
wenzelm
parents: 56831
diff changeset
    61
  {
13f4056c42d7 clarified order;
wenzelm
parents: 56831
diff changeset
    62
    val main_contents =
13f4056c42d7 clarified order;
wenzelm
parents: 56831
diff changeset
    63
      for {
13f4056c42d7 clarified order;
wenzelm
parents: 56831
diff changeset
    64
        (dir, line) <- contents_lines()
13f4056c42d7 clarified order;
wenzelm
parents: 56831
diff changeset
    65
        entry <-
13f4056c42d7 clarified order;
wenzelm
parents: 56831
diff changeset
    66
          line match {
13f4056c42d7 clarified order;
wenzelm
parents: 56831
diff changeset
    67
            case Section_Entry(text) =>
13f4056c42d7 clarified order;
wenzelm
parents: 56831
diff changeset
    68
              Library.try_unsuffix("!", text) match {
13f4056c42d7 clarified order;
wenzelm
parents: 56831
diff changeset
    69
                case None => Some(Section(text, false))
13f4056c42d7 clarified order;
wenzelm
parents: 56831
diff changeset
    70
                case Some(txt) => Some(Section(txt, true))
13f4056c42d7 clarified order;
wenzelm
parents: 56831
diff changeset
    71
              }
13f4056c42d7 clarified order;
wenzelm
parents: 56831
diff changeset
    72
            case Doc_Entry(name, title) => Some(Doc(name, title, dir + Path.basic(name)))
13f4056c42d7 clarified order;
wenzelm
parents: 56831
diff changeset
    73
            case _ => None
13f4056c42d7 clarified order;
wenzelm
parents: 56831
diff changeset
    74
          }
13f4056c42d7 clarified order;
wenzelm
parents: 56831
diff changeset
    75
      } yield entry
13f4056c42d7 clarified order;
wenzelm
parents: 56831
diff changeset
    76
13f4056c42d7 clarified order;
wenzelm
parents: 56831
diff changeset
    77
    examples() ::: release_notes() ::: main_contents
13f4056c42d7 clarified order;
wenzelm
parents: 56831
diff changeset
    78
  }
52427
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    79
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    80
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    81
  /* view */
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    82
56422
7490555d7dff clarified Doc entry: more explicit path;
wenzelm
parents: 56276
diff changeset
    83
  def view(path: Path)
52427
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    84
  {
56831
e3ccf0809d51 prefer scala.Console with its support for thread-local redirection;
wenzelm
parents: 56784
diff changeset
    85
    if (path.is_file) Console.println(Library.trim_line(File.read(path)))
56422
7490555d7dff clarified Doc entry: more explicit path;
wenzelm
parents: 56276
diff changeset
    86
    else {
7490555d7dff clarified Doc entry: more explicit path;
wenzelm
parents: 56276
diff changeset
    87
      val pdf = path.ext("pdf")
7490555d7dff clarified Doc entry: more explicit path;
wenzelm
parents: 56276
diff changeset
    88
      if (pdf.is_file) Isabelle_System.pdf_viewer(pdf)
7490555d7dff clarified Doc entry: more explicit path;
wenzelm
parents: 56276
diff changeset
    89
      else error("Bad Isabelle documentation file: " + pdf)
52427
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    90
    }
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    91
  }
52444
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52429
diff changeset
    92
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52429
diff changeset
    93
62831
5560905a32ae prefer internal tool;
wenzelm
parents: 62454
diff changeset
    94
  /* Isabelle tool wrapper */
52444
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52429
diff changeset
    95
62831
5560905a32ae prefer internal tool;
wenzelm
parents: 62454
diff changeset
    96
  val isabelle_tool = Isabelle_Tool("doc", "view Isabelle documentation", args =>
52444
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52429
diff changeset
    97
  {
62831
5560905a32ae prefer internal tool;
wenzelm
parents: 62454
diff changeset
    98
    val getopts = Getopts("""
62438
42e13a4f52f5 moved getopts to Scala;
wenzelm
parents: 61157
diff changeset
    99
Usage: isabelle doc [DOC ...]
42e13a4f52f5 moved getopts to Scala;
wenzelm
parents: 61157
diff changeset
   100
42e13a4f52f5 moved getopts to Scala;
wenzelm
parents: 61157
diff changeset
   101
  View Isabelle documentation.
42e13a4f52f5 moved getopts to Scala;
wenzelm
parents: 61157
diff changeset
   102
""")
62831
5560905a32ae prefer internal tool;
wenzelm
parents: 62454
diff changeset
   103
    val docs = getopts(args)
62438
42e13a4f52f5 moved getopts to Scala;
wenzelm
parents: 61157
diff changeset
   104
62831
5560905a32ae prefer internal tool;
wenzelm
parents: 62454
diff changeset
   105
    val entries = contents()
5560905a32ae prefer internal tool;
wenzelm
parents: 62454
diff changeset
   106
    if (docs.isEmpty) Console.println(cat_lines(contents_lines().map(_._2)))
5560905a32ae prefer internal tool;
wenzelm
parents: 62454
diff changeset
   107
    else {
5560905a32ae prefer internal tool;
wenzelm
parents: 62454
diff changeset
   108
      docs.foreach(doc =>
5560905a32ae prefer internal tool;
wenzelm
parents: 62454
diff changeset
   109
        entries.collectFirst { case Doc(name, _, path) if doc == name => path } match {
5560905a32ae prefer internal tool;
wenzelm
parents: 62454
diff changeset
   110
          case Some(path) => view(path)
5560905a32ae prefer internal tool;
wenzelm
parents: 62454
diff changeset
   111
          case None => error("No Isabelle documentation entry: " + quote(doc))
5560905a32ae prefer internal tool;
wenzelm
parents: 62454
diff changeset
   112
        }
5560905a32ae prefer internal tool;
wenzelm
parents: 62454
diff changeset
   113
      )
52444
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52429
diff changeset
   114
    }
62831
5560905a32ae prefer internal tool;
wenzelm
parents: 62454
diff changeset
   115
  })
52427
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
   116
}