src/Pure/Tools/doc.scala
author wenzelm
Sat, 21 Sep 2013 19:48:46 +0200
changeset 53777 06a6216f733e
parent 52740 bceec99254b0
child 53935 59c6dbdf0a38
permissions -rw-r--r--
immediate access to some elementary examples;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
52444
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52429
diff changeset
     1
/*  Title:      Pure/Tools/doc.scala
52427
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
     3
52444
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52429
diff changeset
     4
View Isabelle documentation.
52427
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
     5
*/
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
     6
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
     7
package isabelle
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
     8
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
     9
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    10
import scala.util.matching.Regex
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    11
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    12
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    13
object Doc
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    14
{
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    15
  /* dirs */
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    16
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    17
  def dirs(): List[Path] =
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    18
    Path.split(Isabelle_System.getenv("ISABELLE_DOCS")).map(dir =>
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    19
      if (dir.is_dir) dir
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    20
      else error("Bad documentation directory: " + dir))
52740
bceec99254b0 documentation is always in PDF;
wenzelm
parents: 52542
diff changeset
    21
52427
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    22
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    23
  /* contents */
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    24
52444
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52429
diff changeset
    25
  private def contents_lines(): List[String] =
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52429
diff changeset
    26
    for {
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52429
diff changeset
    27
      dir <- dirs()
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52429
diff changeset
    28
      catalog = dir + Path.basic("Contents")
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52429
diff changeset
    29
      if catalog.is_file
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52429
diff changeset
    30
      line <- split_lines(Library.trim_line(File.read(catalog)))
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52429
diff changeset
    31
    } yield line
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52429
diff changeset
    32
52427
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    33
  sealed abstract class Entry
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    34
  case class Section(text: String) extends Entry
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    35
  case class Doc(name: String, title: String) extends Entry
52542
19d674acb764 more release notes according to availability in proper release vs. repository clone;
wenzelm
parents: 52541
diff changeset
    36
  case class Text_File(name: String, path: Path) extends Entry
52427
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    37
53777
06a6216f733e immediate access to some elementary examples;
wenzelm
parents: 52740
diff changeset
    38
  def text_file(name: String): Option[Text_File] =
06a6216f733e immediate access to some elementary examples;
wenzelm
parents: 52740
diff changeset
    39
  {
06a6216f733e immediate access to some elementary examples;
wenzelm
parents: 52740
diff changeset
    40
    val path = Path.variable("ISABELLE_HOME") + Path.explode(name)
06a6216f733e immediate access to some elementary examples;
wenzelm
parents: 52740
diff changeset
    41
    if (path.is_file) Some(Text_File(name, path))
06a6216f733e immediate access to some elementary examples;
wenzelm
parents: 52740
diff changeset
    42
    else None
06a6216f733e immediate access to some elementary examples;
wenzelm
parents: 52740
diff changeset
    43
  }
06a6216f733e immediate access to some elementary examples;
wenzelm
parents: 52740
diff changeset
    44
52444
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52429
diff changeset
    45
  private val Section_Entry = new Regex("""^(\S.*)\s*$""")
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52429
diff changeset
    46
  private val Doc_Entry = new Regex("""^\s+(\S+)\s+(.+)\s*$""")
52427
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    47
52542
19d674acb764 more release notes according to availability in proper release vs. repository clone;
wenzelm
parents: 52541
diff changeset
    48
  private def release_notes(): List[Entry] =
19d674acb764 more release notes according to availability in proper release vs. repository clone;
wenzelm
parents: 52541
diff changeset
    49
  {
19d674acb764 more release notes according to availability in proper release vs. repository clone;
wenzelm
parents: 52541
diff changeset
    50
    val names =
19d674acb764 more release notes according to availability in proper release vs. repository clone;
wenzelm
parents: 52541
diff changeset
    51
      List("ANNOUNCE", "README", "NEWS", "COPYRIGHT", "CONTRIBUTORS",
19d674acb764 more release notes according to availability in proper release vs. repository clone;
wenzelm
parents: 52541
diff changeset
    52
        "contrib/README", "README_REPOSITORY")
19d674acb764 more release notes according to availability in proper release vs. repository clone;
wenzelm
parents: 52541
diff changeset
    53
    Section("Release notes") ::
19d674acb764 more release notes according to availability in proper release vs. repository clone;
wenzelm
parents: 52541
diff changeset
    54
      (for (name <- names; entry <- text_file(name)) yield entry)
19d674acb764 more release notes according to availability in proper release vs. repository clone;
wenzelm
parents: 52541
diff changeset
    55
  }
52541
97c950217d7f quick access to release notes (imitating website/documentation.html);
wenzelm
parents: 52448
diff changeset
    56
53777
06a6216f733e immediate access to some elementary examples;
wenzelm
parents: 52740
diff changeset
    57
  private def examples(): List[Entry] =
06a6216f733e immediate access to some elementary examples;
wenzelm
parents: 52740
diff changeset
    58
  {
06a6216f733e immediate access to some elementary examples;
wenzelm
parents: 52740
diff changeset
    59
    val names =
06a6216f733e immediate access to some elementary examples;
wenzelm
parents: 52740
diff changeset
    60
      List(
06a6216f733e immediate access to some elementary examples;
wenzelm
parents: 52740
diff changeset
    61
        "src/HOL/ex/Seq.thy",
06a6216f733e immediate access to some elementary examples;
wenzelm
parents: 52740
diff changeset
    62
        "src/HOL/Unix/Unix.thy",
06a6216f733e immediate access to some elementary examples;
wenzelm
parents: 52740
diff changeset
    63
        "src/HOL/Isar_Examples/Drinker.thy")
06a6216f733e immediate access to some elementary examples;
wenzelm
parents: 52740
diff changeset
    64
    Section("Examples") :: names.map(name => text_file(name).get)
06a6216f733e immediate access to some elementary examples;
wenzelm
parents: 52740
diff changeset
    65
  }
06a6216f733e immediate access to some elementary examples;
wenzelm
parents: 52740
diff changeset
    66
52444
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52429
diff changeset
    67
  def contents(): List[Entry] =
52541
97c950217d7f quick access to release notes (imitating website/documentation.html);
wenzelm
parents: 52448
diff changeset
    68
    (for {
52444
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52429
diff changeset
    69
      line <- contents_lines()
52427
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    70
      entry <-
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    71
        line match {
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    72
          case Section_Entry(text) => Some(Section(text))
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    73
          case Doc_Entry(name, title) => Some(Doc(name, title))
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    74
          case _ => None
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    75
        }
53777
06a6216f733e immediate access to some elementary examples;
wenzelm
parents: 52740
diff changeset
    76
    } yield entry) ::: release_notes() ::: examples()
52427
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    77
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    78
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    79
  /* view */
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    80
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    81
  def view(name: String)
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    82
  {
52740
bceec99254b0 documentation is always in PDF;
wenzelm
parents: 52542
diff changeset
    83
    val doc = name + ".pdf"
52448
082a1c8c2c89 clarified ISABELLE_DOC_FORMAT -- eliminated slightly odd fall-back;
wenzelm
parents: 52444
diff changeset
    84
    dirs().find(dir => (dir + Path.basic(doc)).is_file) match {
082a1c8c2c89 clarified ISABELLE_DOC_FORMAT -- eliminated slightly odd fall-back;
wenzelm
parents: 52444
diff changeset
    85
      case Some(dir) =>
52429
921f22c8890e detach process more reliably -- NB: viewer might be synchronous or asynchronous depending on settings;
wenzelm
parents: 52427
diff changeset
    86
        Isabelle_System.bash_env(dir.file, null,
921f22c8890e detach process more reliably -- NB: viewer might be synchronous or asynchronous depending on settings;
wenzelm
parents: 52427
diff changeset
    87
          "\"$ISABELLE_TOOL\" display " + quote(doc) + " >/dev/null 2>/dev/null &")
52448
082a1c8c2c89 clarified ISABELLE_DOC_FORMAT -- eliminated slightly odd fall-back;
wenzelm
parents: 52444
diff changeset
    88
      case None => error("Missing Isabelle documentation file: " + quote(doc))
52427
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    89
    }
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    90
  }
52444
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52429
diff changeset
    91
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52429
diff changeset
    92
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52429
diff changeset
    93
  /* command line entry point */
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52429
diff changeset
    94
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52429
diff changeset
    95
  def main(args: Array[String])
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52429
diff changeset
    96
  {
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52429
diff changeset
    97
    Command_Line.tool {
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52429
diff changeset
    98
      if (args.isEmpty) Console.println(cat_lines(contents_lines()))
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52429
diff changeset
    99
      else args.foreach(view)
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52429
diff changeset
   100
      0
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52429
diff changeset
   101
    }
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52429
diff changeset
   102
  }
52427
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
   103
}
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
   104