src/Pure/Tools/doc.scala
changeset 52542 19d674acb764
parent 52541 97c950217d7f
child 52740 bceec99254b0
     1.1 --- a/src/Pure/Tools/doc.scala	Sat Jul 06 21:51:35 2013 +0200
     1.2 +++ b/src/Pure/Tools/doc.scala	Sat Jul 06 22:11:18 2013 +0200
     1.3 @@ -33,18 +33,25 @@
     1.4    sealed abstract class Entry
     1.5    case class Section(text: String) extends Entry
     1.6    case class Doc(name: String, title: String) extends Entry
     1.7 -  case class Text_File(path: Path) extends Entry
     1.8 +  case class Text_File(name: String, path: Path) extends Entry
     1.9  
    1.10    private val Section_Entry = new Regex("""^(\S.*)\s*$""")
    1.11    private val Doc_Entry = new Regex("""^\s+(\S+)\s+(.+)\s*$""")
    1.12  
    1.13 -  private val release_notes =
    1.14 -    List(Section("Release notes"),
    1.15 -      Text_File(Path.explode("~~/ANNOUNCE")),
    1.16 -      Text_File(Path.explode("~~/README")),
    1.17 -      Text_File(Path.explode("~~/NEWS")),
    1.18 -      Text_File(Path.explode("~~/COPYRIGHT")),
    1.19 -      Text_File(Path.explode("~~/CONTRIBUTORS")))
    1.20 +  private def release_notes(): List[Entry] =
    1.21 +  {
    1.22 +    def text_file(name: String): Option[Text_File] =
    1.23 +    {
    1.24 +      val path = Path.variable("ISABELLE_HOME") + Path.explode(name)
    1.25 +      if (path.is_file) Some(Text_File(name, path))
    1.26 +      else None
    1.27 +    }
    1.28 +    val names =
    1.29 +      List("ANNOUNCE", "README", "NEWS", "COPYRIGHT", "CONTRIBUTORS",
    1.30 +        "contrib/README", "README_REPOSITORY")
    1.31 +    Section("Release notes") ::
    1.32 +      (for (name <- names; entry <- text_file(name)) yield entry)
    1.33 +  }
    1.34  
    1.35    def contents(): List[Entry] =
    1.36      (for {
    1.37 @@ -55,7 +62,7 @@
    1.38            case Doc_Entry(name, title) => Some(Doc(name, title))
    1.39            case _ => None
    1.40          }
    1.41 -    } yield entry) ::: release_notes
    1.42 +    } yield entry) ::: release_notes()
    1.43  
    1.44  
    1.45    /* view */