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