src/Pure/Tools/doc.scala
author wenzelm
Sat Apr 05 18:52:03 2014 +0200 (2014-04-05)
changeset 56423 c2f52824dbb2
parent 56422 7490555d7dff
child 56424 7032378cc097
permissions -rw-r--r--
explicit indication of important doc sections ("!"), which are expanded in the tree view;
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@52740
    21
wenzelm@52427
    22
wenzelm@52427
    23
  /* contents */
wenzelm@52427
    24
wenzelm@56422
    25
  private def contents_lines(): List[(Path, 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@56422
    31
    } yield (dir, line)
wenzelm@52444
    32
wenzelm@52427
    33
  sealed abstract class Entry
wenzelm@56423
    34
  case class Section(text: String, important: Boolean) extends Entry
wenzelm@56422
    35
  case class Doc(name: String, title: String, path: Path) extends Entry
wenzelm@52542
    36
  case class Text_File(name: String, path: Path) extends Entry
wenzelm@52427
    37
wenzelm@53777
    38
  def text_file(name: String): Option[Text_File] =
wenzelm@53777
    39
  {
wenzelm@53777
    40
    val path = Path.variable("ISABELLE_HOME") + Path.explode(name)
wenzelm@53777
    41
    if (path.is_file) Some(Text_File(name, path))
wenzelm@53777
    42
    else None
wenzelm@53777
    43
  }
wenzelm@53777
    44
wenzelm@52444
    45
  private val Section_Entry = new Regex("""^(\S.*)\s*$""")
wenzelm@52444
    46
  private val Doc_Entry = new Regex("""^\s+(\S+)\s+(.+)\s*$""")
wenzelm@52427
    47
wenzelm@52542
    48
  private def release_notes(): List[Entry] =
wenzelm@52542
    49
  {
wenzelm@52542
    50
    val names =
wenzelm@52542
    51
      List("ANNOUNCE", "README", "NEWS", "COPYRIGHT", "CONTRIBUTORS",
wenzelm@52542
    52
        "contrib/README", "README_REPOSITORY")
wenzelm@56423
    53
    Section("Release notes", true) ::
wenzelm@52542
    54
      (for (name <- names; entry <- text_file(name)) yield entry)
wenzelm@52542
    55
  }
wenzelm@52541
    56
wenzelm@53777
    57
  private def examples(): List[Entry] =
wenzelm@53777
    58
  {
wenzelm@53777
    59
    val names =
wenzelm@53777
    60
      List(
wenzelm@53777
    61
        "src/HOL/ex/Seq.thy",
wenzelm@53935
    62
        "src/HOL/ex/ML.thy",
wenzelm@53777
    63
        "src/HOL/Unix/Unix.thy",
wenzelm@56276
    64
        "src/HOL/Isar_Examples/Drinker.thy",
wenzelm@56276
    65
        "src/Tools/SML/Examples.thy")
wenzelm@56423
    66
    Section("Examples", true) :: names.map(name => text_file(name).get)
wenzelm@53777
    67
  }
wenzelm@53777
    68
wenzelm@52444
    69
  def contents(): List[Entry] =
wenzelm@52541
    70
    (for {
wenzelm@56422
    71
      (dir, line) <- contents_lines()
wenzelm@52427
    72
      entry <-
wenzelm@52427
    73
        line match {
wenzelm@56423
    74
          case Section_Entry(text) =>
wenzelm@56423
    75
            Library.try_unsuffix("!", text) match {
wenzelm@56423
    76
              case None => Some(Section(text, false))
wenzelm@56423
    77
              case Some(txt) => Some(Section(txt, true))
wenzelm@56423
    78
            }
wenzelm@56422
    79
          case Doc_Entry(name, title) => Some(Doc(name, title, dir + Path.basic(name)))
wenzelm@52427
    80
          case _ => None
wenzelm@52427
    81
        }
wenzelm@53777
    82
    } yield entry) ::: release_notes() ::: examples()
wenzelm@52427
    83
wenzelm@52427
    84
wenzelm@52427
    85
  /* view */
wenzelm@52427
    86
wenzelm@56422
    87
  def view(path: Path)
wenzelm@52427
    88
  {
wenzelm@56422
    89
    if (path.is_file) Console.println(File.read(path))
wenzelm@56422
    90
    else {
wenzelm@56422
    91
      val pdf = path.ext("pdf")
wenzelm@56422
    92
      if (pdf.is_file) Isabelle_System.pdf_viewer(pdf)
wenzelm@56422
    93
      else error("Bad Isabelle documentation file: " + pdf)
wenzelm@52427
    94
    }
wenzelm@52427
    95
  }
wenzelm@52444
    96
wenzelm@52444
    97
wenzelm@52444
    98
  /* command line entry point */
wenzelm@52444
    99
wenzelm@52444
   100
  def main(args: Array[String])
wenzelm@52444
   101
  {
wenzelm@52444
   102
    Command_Line.tool {
wenzelm@56422
   103
      if (args.isEmpty) Console.println(cat_lines(contents_lines().map(_._2)))
wenzelm@56422
   104
      else {
wenzelm@56422
   105
        val entries = contents()
wenzelm@56422
   106
        args.foreach(arg =>
wenzelm@56422
   107
          entries.collectFirst { case Doc(name, _, path) if arg == name => path } match {
wenzelm@56422
   108
            case Some(path) => view(path)
wenzelm@56422
   109
            case None => error("No Isabelle documentation entry: " + quote(arg))
wenzelm@56422
   110
          }
wenzelm@56422
   111
        )
wenzelm@56422
   112
      }
wenzelm@52444
   113
      0
wenzelm@52444
   114
    }
wenzelm@52444
   115
  }
wenzelm@52427
   116
}
wenzelm@52427
   117