src/Pure/Tools/doc.scala
changeset 56424 7032378cc097
parent 56423 c2f52824dbb2
child 56425 d12653fbd5b1
     1.1 --- a/src/Pure/Tools/doc.scala	Sat Apr 05 18:52:03 2014 +0200
     1.2 +++ b/src/Pure/Tools/doc.scala	Sat Apr 05 19:07:05 2014 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  /*  Title:      Pure/Tools/doc.scala
     1.5      Author:     Makarius
     1.6  
     1.7 -View Isabelle documentation.
     1.8 +Access to Isabelle documentation.
     1.9  */
    1.10  
    1.11  package isabelle
    1.12 @@ -35,10 +35,10 @@
    1.13    case class Doc(name: String, title: String, path: Path) extends Entry
    1.14    case class Text_File(name: String, path: Path) extends Entry
    1.15  
    1.16 -  def text_file(name: String): Option[Text_File] =
    1.17 +  def text_file(name: Path): Option[Text_File] =
    1.18    {
    1.19 -    val path = Path.variable("ISABELLE_HOME") + Path.explode(name)
    1.20 -    if (path.is_file) Some(Text_File(name, path))
    1.21 +    val path = Path.variable("ISABELLE_HOME") + name
    1.22 +    if (path.is_file) Some(Text_File(name.implode, path))
    1.23      else None
    1.24    }
    1.25  
    1.26 @@ -46,25 +46,16 @@
    1.27    private val Doc_Entry = new Regex("""^\s+(\S+)\s+(.+)\s*$""")
    1.28  
    1.29    private def release_notes(): List[Entry] =
    1.30 -  {
    1.31 -    val names =
    1.32 -      List("ANNOUNCE", "README", "NEWS", "COPYRIGHT", "CONTRIBUTORS",
    1.33 -        "contrib/README", "README_REPOSITORY")
    1.34      Section("Release notes", true) ::
    1.35 -      (for (name <- names; entry <- text_file(name)) yield entry)
    1.36 -  }
    1.37 +      Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_RELEASE_NOTES")).flatMap(text_file(_))
    1.38  
    1.39    private def examples(): List[Entry] =
    1.40 -  {
    1.41 -    val names =
    1.42 -      List(
    1.43 -        "src/HOL/ex/Seq.thy",
    1.44 -        "src/HOL/ex/ML.thy",
    1.45 -        "src/HOL/Unix/Unix.thy",
    1.46 -        "src/HOL/Isar_Examples/Drinker.thy",
    1.47 -        "src/Tools/SML/Examples.thy")
    1.48 -    Section("Examples", true) :: names.map(name => text_file(name).get)
    1.49 -  }
    1.50 +    Section("Examples", true) ::
    1.51 +      Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_EXAMPLES")).map(file =>
    1.52 +        text_file(file) match {
    1.53 +          case Some(entry) => entry
    1.54 +          case None => error("Bad ISABELLE_DOCS_EXAMPLES entry: " + file)
    1.55 +        })
    1.56  
    1.57    def contents(): List[Entry] =
    1.58      (for {