src/Pure/System/doc.scala
author wenzelm
Sun, 23 Jun 2013 21:15:42 +0200
changeset 52429 921f22c8890e
parent 52427 9d1cc9a22177
permissions -rw-r--r--
detach process more reliably -- NB: viewer might be synchronous or asynchronous depending on settings;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
52427
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/System/doc.scala
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
     3
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
     4
View Isabelle documentation (see also "isabelle doc").
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))
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    21
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
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    25
  sealed abstract class Entry
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    26
  case class Section(text: String) extends Entry
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    27
  case class Doc(name: String, title: String) extends Entry
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    28
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    29
  def contents(): List[Entry] =
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    30
  {
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    31
    val Section_Entry = new Regex("""^(\S.*)\s*$""")
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    32
    val Doc_Entry = new Regex("""^\s+(\S+)\s+(.+)\s*$""")
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    33
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    34
    for {
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    35
      dir <- dirs()
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    36
      catalog = dir + Path.basic("Contents")
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    37
      if catalog.is_file
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    38
      line <- split_lines(File.read(catalog))
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    39
      entry <-
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    40
        line match {
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    41
          case Section_Entry(text) => Some(Section(text))
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    42
          case Doc_Entry(name, title) => Some(Doc(name, title))
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    43
          case _ => None
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    44
        }
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    45
    } yield entry
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    46
  }
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    47
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    48
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    49
  /* view */
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    50
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    51
  def view(name: String)
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    52
  {
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    53
    val formats = List(Isabelle_System.getenv_strict("ISABELLE_DOC_FORMAT"), "dvi")
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    54
    val docs =
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    55
      for {
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    56
        dir <- dirs()
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    57
        fmt <- formats
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    58
        doc = name + "." + fmt
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    59
        if (dir + Path.basic(doc)).is_file
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    60
      } yield (dir, doc)
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    61
    docs match {
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    62
      case (dir, doc) :: _ =>
52429
921f22c8890e detach process more reliably -- NB: viewer might be synchronous or asynchronous depending on settings;
wenzelm
parents: 52427
diff changeset
    63
        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
    64
          "\"$ISABELLE_TOOL\" display " + quote(doc) + " >/dev/null 2>/dev/null &")
52427
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    65
      case Nil => error("Missing Isabelle documentation: " + quote(name))
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    66
    }
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    67
  }
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    68
}
9d1cc9a22177 Scala version of "isabelle doc";
wenzelm
parents:
diff changeset
    69