1.1 --- a/etc/settings	Sat Apr 05 18:52:03 2014 +0200
     1.2 +++ b/etc/settings	Sat Apr 05 19:07:05 2014 +0200
     1.3 @@ -101,6 +101,9 @@
     1.4  # Where to look for docs (multiple dirs separated by ':').
     1.5  ISABELLE_DOCS="$ISABELLE_HOME/doc"
     1.6  
     1.7 +ISABELLE_DOCS_RELEASE_NOTES="ANNOUNCE:README:NEWS:COPYRIGHT:CONTRIBUTORS:contrib/README:README_REPOSITORY"
     1.8 +ISABELLE_DOCS_EXAMPLES="src/HOL/ex/Seq.thy:src/HOL/ex/ML.thy:src/HOL/Unix/Unix.thy:src/HOL/Isar_Examples/Drinker.thy:src/Tools/SML/Examples.thy"
     1.9 +
    1.10  # "open" within desktop environment (potentially asynchronous)
    1.11  case "$ISABELLE_PLATFORM_FAMILY" in
    1.12    linux)

     2.1 --- a/src/Pure/Tools/doc.scala	Sat Apr 05 18:52:03 2014 +0200
     2.2 +++ b/src/Pure/Tools/doc.scala	Sat Apr 05 19:07:05 2014 +0200
     2.3 @@ -1,7 +1,7 @@
     2.4  /*  Title:      Pure/Tools/doc.scala
     2.5      Author:     Makarius
     2.6  
     2.7 -View Isabelle documentation.
     2.8 +Access to Isabelle documentation.
     2.9  */
    2.10  
    2.11  package isabelle
    2.12 @@ -35,10 +35,10 @@
    2.13    case class Doc(name: String, title: String, path: Path) extends Entry
    2.14    case class Text_File(name: String, path: Path) extends Entry
    2.15  
    2.16 -  def text_file(name: String): Option[Text_File] =
    2.17 +  def text_file(name: Path): Option[Text_File] =
    2.18    {
    2.19 -    val path = Path.variable("ISABELLE_HOME") + Path.explode(name)
    2.20 -    if (path.is_file) Some(Text_File(name, path))
    2.21 +    val path = Path.variable("ISABELLE_HOME") + name
    2.22 +    if (path.is_file) Some(Text_File(name.implode, path))
    2.23      else None
    2.24    }
    2.25  
    2.26 @@ -46,25 +46,16 @@
    2.27    private val Doc_Entry = new Regex("""^\s+(\S+)\s+(.+)\s*$""")
    2.28  
    2.29    private def release_notes(): List[Entry] =
    2.30 -  {
    2.31 -    val names =
    2.32 -      List("ANNOUNCE", "README", "NEWS", "COPYRIGHT", "CONTRIBUTORS",
    2.33 -        "contrib/README", "README_REPOSITORY")
    2.34      Section("Release notes", true) ::
    2.35 -      (for (name <- names; entry <- text_file(name)) yield entry)
    2.36 -  }
    2.37 +      Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_RELEASE_NOTES")).flatMap(text_file(_))
    2.38  
    2.39    private def examples(): List[Entry] =
    2.40 -  {
    2.41 -    val names =
    2.42 -      List(
    2.43 -        "src/HOL/ex/Seq.thy",
    2.44 -        "src/HOL/ex/ML.thy",
    2.45 -        "src/HOL/Unix/Unix.thy",
    2.46 -        "src/HOL/Isar_Examples/Drinker.thy",
    2.47 -        "src/Tools/SML/Examples.thy")
    2.48 -    Section("Examples", true) :: names.map(name => text_file(name).get)
    2.49 -  }
    2.50 +    Section("Examples", true) ::
    2.51 +      Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_EXAMPLES")).map(file =>
    2.52 +        text_file(file) match {
    2.53 +          case Some(entry) => entry
    2.54 +          case None => error("Bad ISABELLE_DOCS_EXAMPLES entry: " + file)
    2.55 +        })
    2.56  
    2.57    def contents(): List[Entry] =
    2.58      (for {