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);
wenzelm@52444
     1
/*  Title:      Pure/Tools/doc.scala
wenzelm@52427
     2
    Author:     Makarius
wenzelm@52427
     3
wenzelm@52444
     4
View Isabelle documentation.
wenzelm@52427
     5
*/
wenzelm@52427
     6
wenzelm@52427
     7
package isabelle
wenzelm@52427
     8
wenzelm@52427
     9
wenzelm@52427
    10
import scala.util.matching.Regex
wenzelm@52427
    11
wenzelm@52427
    12
wenzelm@52427
    13
object Doc
wenzelm@52427
    14
{
wenzelm@52427
    15
  /* dirs */
wenzelm@52427
    16
wenzelm@52427
    17
  def dirs(): List[Path] =
wenzelm@52427
    18
    Path.split(Isabelle_System.getenv("ISABELLE_DOCS")).map(dir =>
wenzelm@52427
    19
      if (dir.is_dir) dir
wenzelm@52427
    20
      else error("Bad documentation directory: " + dir))
wenzelm@52541
    21
    
wenzelm@52427
    22
wenzelm@52427
    23
  /* contents */
wenzelm@52427
    24
wenzelm@52444
    25
  private def contents_lines(): List[String] =
wenzelm@52444
    26
    for {
wenzelm@52444
    27
      dir <- dirs()
wenzelm@52444
    28
      catalog = dir + Path.basic("Contents")
wenzelm@52444
    29
      if catalog.is_file
wenzelm@52444
    30
      line <- split_lines(Library.trim_line(File.read(catalog)))
wenzelm@52444
    31
    } yield line
wenzelm@52444
    32
wenzelm@52427
    33
  sealed abstract class Entry
wenzelm@52427
    34
  case class Section(text: String) extends Entry
wenzelm@52427
    35
  case class Doc(name: String, title: String) extends Entry
wenzelm@52541
    36
  case class Text_File(path: Path) extends Entry
wenzelm@52427
    37
wenzelm@52444
    38
  private val Section_Entry = new Regex("""^(\S.*)\s*$""")
wenzelm@52444
    39
  private val Doc_Entry = new Regex("""^\s+(\S+)\s+(.+)\s*$""")
wenzelm@52427
    40
wenzelm@52541
    41
  private val release_notes =
wenzelm@52541
    42
    List(Section("Release notes"),
wenzelm@52541
    43
      Text_File(Path.explode("~~/ANNOUNCE")),
wenzelm@52541
    44
      Text_File(Path.explode("~~/README")),
wenzelm@52541
    45
      Text_File(Path.explode("~~/NEWS")),
wenzelm@52541
    46
      Text_File(Path.explode("~~/COPYRIGHT")),
wenzelm@52541
    47
      Text_File(Path.explode("~~/CONTRIBUTORS")))
wenzelm@52541
    48
wenzelm@52444
    49
  def contents(): List[Entry] =
wenzelm@52541
    50
    (for {
wenzelm@52444
    51
      line <- contents_lines()
wenzelm@52427
    52
      entry <-
wenzelm@52427
    53
        line match {
wenzelm@52427
    54
          case Section_Entry(text) => Some(Section(text))
wenzelm@52427
    55
          case Doc_Entry(name, title) => Some(Doc(name, title))
wenzelm@52427
    56
          case _ => None
wenzelm@52427
    57
        }
wenzelm@52541
    58
    } yield entry) ::: release_notes
wenzelm@52427
    59
wenzelm@52427
    60
wenzelm@52427
    61
  /* view */
wenzelm@52427
    62
wenzelm@52427
    63
  def view(name: String)
wenzelm@52427
    64
  {
wenzelm@52448
    65
    val doc = name + "." + Isabelle_System.getenv_strict("ISABELLE_DOC_FORMAT")
wenzelm@52448
    66
    dirs().find(dir => (dir + Path.basic(doc)).is_file) match {
wenzelm@52448
    67
      case Some(dir) =>
wenzelm@52429
    68
        Isabelle_System.bash_env(dir.file, null,
wenzelm@52429
    69
          "\"$ISABELLE_TOOL\" display " + quote(doc) + " >/dev/null 2>/dev/null &")
wenzelm@52448
    70
      case None => error("Missing Isabelle documentation file: " + quote(doc))
wenzelm@52427
    71
    }
wenzelm@52427
    72
  }
wenzelm@52444
    73
wenzelm@52444
    74
wenzelm@52444
    75
  /* command line entry point */
wenzelm@52444
    76
wenzelm@52444
    77
  def main(args: Array[String])
wenzelm@52444
    78
  {
wenzelm@52444
    79
    Command_Line.tool {
wenzelm@52444
    80
      if (args.isEmpty) Console.println(cat_lines(contents_lines()))
wenzelm@52444
    81
      else args.foreach(view)
wenzelm@52444
    82
      0
wenzelm@52444
    83
    }
wenzelm@52444
    84
  }
wenzelm@52427
    85
}
wenzelm@52427
    86