src/Pure/Tools/doc.scala
author wenzelm
Tue Mar 25 14:52:35 2014 +0100 (2014-03-25)
changeset 56276 9e2d5e3debd3
parent 54690 cd88b44623bf
child 56422 7490555d7dff
permissions -rw-r--r--
some SML examples;
     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   def text_file(name: String): Option[Text_File] =
    39   {
    40     val path = Path.variable("ISABELLE_HOME") + Path.explode(name)
    41     if (path.is_file) Some(Text_File(name, 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   {
    50     val names =
    51       List("ANNOUNCE", "README", "NEWS", "COPYRIGHT", "CONTRIBUTORS",
    52         "contrib/README", "README_REPOSITORY")
    53     Section("Release notes") ::
    54       (for (name <- names; entry <- text_file(name)) yield entry)
    55   }
    56 
    57   private def examples(): List[Entry] =
    58   {
    59     val names =
    60       List(
    61         "src/HOL/ex/Seq.thy",
    62         "src/HOL/ex/ML.thy",
    63         "src/HOL/Unix/Unix.thy",
    64         "src/HOL/Isar_Examples/Drinker.thy",
    65         "src/Tools/SML/Examples.thy")
    66     Section("Examples") :: names.map(name => text_file(name).get)
    67   }
    68 
    69   def contents(): List[Entry] =
    70     (for {
    71       line <- contents_lines()
    72       entry <-
    73         line match {
    74           case Section_Entry(text) => Some(Section(text))
    75           case Doc_Entry(name, title) => Some(Doc(name, title))
    76           case _ => None
    77         }
    78     } yield entry) ::: release_notes() ::: examples()
    79 
    80 
    81   /* view */
    82 
    83   def view(name: String)
    84   {
    85     val doc = Path.basic(name + ".pdf")
    86     dirs().find(dir => (dir + doc).is_file) match {
    87       case Some(dir) => Isabelle_System.pdf_viewer(dir + doc)
    88       case None => error("Missing Isabelle documentation file: " + doc)
    89     }
    90   }
    91 
    92 
    93   /* command line entry point */
    94 
    95   def main(args: Array[String])
    96   {
    97     Command_Line.tool {
    98       if (args.isEmpty) Console.println(cat_lines(contents_lines()))
    99       else args.foreach(view)
   100       0
   101     }
   102   }
   103 }
   104