src/Pure/Tools/doc.scala
author wenzelm
Tue Jun 25 12:17:19 2013 +0200 (2013-06-25)
changeset 52444 2cfe6656d6d6
parent 52429 src/Pure/System/doc.scala@921f22c8890e
child 52448 082a1c8c2c89
permissions -rw-r--r--
slightly improved "isabelle doc" based on Isabelle/Scala;
updated documentation of "isabelle display";
     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 
    37   private val Section_Entry = new Regex("""^(\S.*)\s*$""")
    38   private val Doc_Entry = new Regex("""^\s+(\S+)\s+(.+)\s*$""")
    39 
    40   def contents(): List[Entry] =
    41     for {
    42       line <- contents_lines()
    43       entry <-
    44         line match {
    45           case Section_Entry(text) => Some(Section(text))
    46           case Doc_Entry(name, title) => Some(Doc(name, title))
    47           case _ => None
    48         }
    49     } yield entry
    50 
    51 
    52   /* view */
    53 
    54   def view(name: String)
    55   {
    56     val formats = List(Isabelle_System.getenv_strict("ISABELLE_DOC_FORMAT"), "dvi")
    57     val docs =
    58       for {
    59         dir <- dirs()
    60         fmt <- formats
    61         doc = name + "." + fmt
    62         if (dir + Path.basic(doc)).is_file
    63       } yield (dir, doc)
    64     docs match {
    65       case (dir, doc) :: _ =>
    66         Isabelle_System.bash_env(dir.file, null,
    67           "\"$ISABELLE_TOOL\" display " + quote(doc) + " >/dev/null 2>/dev/null &")
    68       case Nil => error("Missing Isabelle documentation: " + quote(name))
    69     }
    70   }
    71 
    72 
    73   /* command line entry point */
    74 
    75   def main(args: Array[String])
    76   {
    77     Command_Line.tool {
    78       if (args.isEmpty) Console.println(cat_lines(contents_lines()))
    79       else args.foreach(view)
    80       0
    81     }
    82   }
    83 }
    84