src/Pure/Tools/doc.scala
author wenzelm
Sat Jul 27 21:01:35 2013 +0200 (2013-07-27)
changeset 52740 bceec99254b0
parent 52542 19d674acb764
child 53777 06a6216f733e
permissions -rw-r--r--
documentation is always in PDF;
     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(name: String, 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 def release_notes(): List[Entry] =
    42   {
    43     def text_file(name: String): Option[Text_File] =
    44     {
    45       val path = Path.variable("ISABELLE_HOME") + Path.explode(name)
    46       if (path.is_file) Some(Text_File(name, path))
    47       else None
    48     }
    49     val names =
    50       List("ANNOUNCE", "README", "NEWS", "COPYRIGHT", "CONTRIBUTORS",
    51         "contrib/README", "README_REPOSITORY")
    52     Section("Release notes") ::
    53       (for (name <- names; entry <- text_file(name)) yield entry)
    54   }
    55 
    56   def contents(): List[Entry] =
    57     (for {
    58       line <- contents_lines()
    59       entry <-
    60         line match {
    61           case Section_Entry(text) => Some(Section(text))
    62           case Doc_Entry(name, title) => Some(Doc(name, title))
    63           case _ => None
    64         }
    65     } yield entry) ::: release_notes()
    66 
    67 
    68   /* view */
    69 
    70   def view(name: String)
    71   {
    72     val doc = name + ".pdf"
    73     dirs().find(dir => (dir + Path.basic(doc)).is_file) match {
    74       case Some(dir) =>
    75         Isabelle_System.bash_env(dir.file, null,
    76           "\"$ISABELLE_TOOL\" display " + quote(doc) + " >/dev/null 2>/dev/null &")
    77       case None => error("Missing Isabelle documentation file: " + quote(doc))
    78     }
    79   }
    80 
    81 
    82   /* command line entry point */
    83 
    84   def main(args: Array[String])
    85   {
    86     Command_Line.tool {
    87       if (args.isEmpty) Console.println(cat_lines(contents_lines()))
    88       else args.foreach(view)
    89       0
    90     }
    91   }
    92 }
    93