src/Pure/Tools/doc.scala
author wenzelm
Sat Jul 06 21:51:35 2013 +0200 (2013-07-06)
changeset 52541 97c950217d7f
parent 52448 082a1c8c2c89
child 52542 19d674acb764
permissions -rw-r--r--
quick access to release notes (imitating website/documentation.html);
     1 /*  Title:      Pure/Tools/doc.scala
     2     Author:     Makarius
     3 
     4 View 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[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 line
    32 
    33   sealed abstract class Entry
    34   case class Section(text: String) extends Entry
    35   case class Doc(name: String, title: String) extends Entry
    36   case class Text_File(path: Path) extends Entry
    37 
    38   private val Section_Entry = new Regex("""^(\S.*)\s*$""")
    39   private val Doc_Entry = new Regex("""^\s+(\S+)\s+(.+)\s*$""")
    40 
    41   private val release_notes =
    42     List(Section("Release notes"),
    43       Text_File(Path.explode("~~/ANNOUNCE")),
    44       Text_File(Path.explode("~~/README")),
    45       Text_File(Path.explode("~~/NEWS")),
    46       Text_File(Path.explode("~~/COPYRIGHT")),
    47       Text_File(Path.explode("~~/CONTRIBUTORS")))
    48 
    49   def contents(): List[Entry] =
    50     (for {
    51       line <- contents_lines()
    52       entry <-
    53         line match {
    54           case Section_Entry(text) => Some(Section(text))
    55           case Doc_Entry(name, title) => Some(Doc(name, title))
    56           case _ => None
    57         }
    58     } yield entry) ::: release_notes
    59 
    60 
    61   /* view */
    62 
    63   def view(name: String)
    64   {
    65     val doc = name + "." + Isabelle_System.getenv_strict("ISABELLE_DOC_FORMAT")
    66     dirs().find(dir => (dir + Path.basic(doc)).is_file) match {
    67       case Some(dir) =>
    68         Isabelle_System.bash_env(dir.file, null,
    69           "\"$ISABELLE_TOOL\" display " + quote(doc) + " >/dev/null 2>/dev/null &")
    70       case None => error("Missing Isabelle documentation file: " + quote(doc))
    71     }
    72   }
    73 
    74 
    75   /* command line entry point */
    76 
    77   def main(args: Array[String])
    78   {
    79     Command_Line.tool {
    80       if (args.isEmpty) Console.println(cat_lines(contents_lines()))
    81       else args.foreach(view)
    82       0
    83     }
    84   }
    85 }
    86