src/Pure/Tools/doc.scala
author wenzelm
Sat Feb 27 19:57:36 2016 +0100 (2016-02-27)
changeset 62438 42e13a4f52f5
parent 61157 13f4056c42d7
child 62454 38c89353b349
permissions -rw-r--r--
moved getopts to Scala;
     1 /*  Title:      Pure/Tools/doc.scala
     2     Author:     Makarius
     3 
     4 Access to Isabelle documentation.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import scala.util.matching.Regex
    11 
    12 
    13 object Doc
    14 {
    15   /* dirs */
    16 
    17   def dirs(): List[Path] =
    18     Path.split(Isabelle_System.getenv("ISABELLE_DOCS")).map(dir =>
    19       if (dir.is_dir) dir
    20       else error("Bad documentation directory: " + dir))
    21 
    22 
    23   /* contents */
    24 
    25   private def contents_lines(): List[(Path, String)] =
    26     for {
    27       dir <- dirs()
    28       catalog = dir + Path.basic("Contents")
    29       if catalog.is_file
    30       line <- split_lines(Library.trim_line(File.read(catalog)))
    31     } yield (dir, line)
    32 
    33   sealed abstract class Entry
    34   case class Section(text: String, important: Boolean) extends Entry
    35   case class Doc(name: String, title: String, path: Path) extends Entry
    36   case class Text_File(name: String, path: Path) extends Entry
    37 
    38   def text_file(name: Path): Option[Text_File] =
    39   {
    40     val path = Path.variable("ISABELLE_HOME") + name
    41     if (path.is_file) Some(Text_File(name.implode, path))
    42     else None
    43   }
    44 
    45   private val Section_Entry = new Regex("""^(\S.*)\s*$""")
    46   private val Doc_Entry = new Regex("""^\s+(\S+)\s+(.+)\s*$""")
    47 
    48   private def release_notes(): List[Entry] =
    49     Section("Release notes", true) ::
    50       Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_RELEASE_NOTES")).flatMap(text_file(_))
    51 
    52   private def examples(): List[Entry] =
    53     Section("Examples", true) ::
    54       Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_EXAMPLES")).map(file =>
    55         text_file(file) match {
    56           case Some(entry) => entry
    57           case None => error("Bad entry in ISABELLE_DOCS_EXAMPLES: " + file)
    58         })
    59 
    60   def contents(): List[Entry] =
    61   {
    62     val main_contents =
    63       for {
    64         (dir, line) <- contents_lines()
    65         entry <-
    66           line match {
    67             case Section_Entry(text) =>
    68               Library.try_unsuffix("!", text) match {
    69                 case None => Some(Section(text, false))
    70                 case Some(txt) => Some(Section(txt, true))
    71               }
    72             case Doc_Entry(name, title) => Some(Doc(name, title, dir + Path.basic(name)))
    73             case _ => None
    74           }
    75       } yield entry
    76 
    77     examples() ::: release_notes() ::: main_contents
    78   }
    79 
    80 
    81   /* view */
    82 
    83   def view(path: Path)
    84   {
    85     if (path.is_file) Console.println(Library.trim_line(File.read(path)))
    86     else {
    87       val pdf = path.ext("pdf")
    88       if (pdf.is_file) Isabelle_System.pdf_viewer(pdf)
    89       else error("Bad Isabelle documentation file: " + pdf)
    90     }
    91   }
    92 
    93 
    94   /* command line entry point */
    95 
    96   def main(args: Array[String])
    97   {
    98     Command_Line.tool0 {
    99       val getopts = Getopts(() => """
   100 Usage: isabelle doc [DOC ...]
   101 
   102   View Isabelle documentation.
   103 """)
   104       val docs = getopts(args)
   105 
   106       val entries = contents()
   107       if (docs.isEmpty) Console.println(cat_lines(contents_lines().map(_._2)))
   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 }