# HG changeset patch
# User wenzelm
# Date 1396717625 -7200
# Node ID 7032378cc0975264fc6fb9c2c49f12ca09d2d81a
# Parent  c2f52824dbb297e3e8cf751e3d33c20f82b8b325
proper settings instead of hard-wired information;

diff -r c2f52824dbb2 -r 7032378cc097 etc/settings
--- a/etc/settings	Sat Apr 05 18:52:03 2014 +0200
+++ b/etc/settings	Sat Apr 05 19:07:05 2014 +0200
@@ -101,6 +101,9 @@
 # Where to look for docs (multiple dirs separated by ':').
 ISABELLE_DOCS="$ISABELLE_HOME/doc"
 
+ISABELLE_DOCS_RELEASE_NOTES="ANNOUNCE:README:NEWS:COPYRIGHT:CONTRIBUTORS:contrib/README:README_REPOSITORY"
+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"
+
 # "open" within desktop environment (potentially asynchronous)
 case "$ISABELLE_PLATFORM_FAMILY" in
   linux)
diff -r c2f52824dbb2 -r 7032378cc097 src/Pure/Tools/doc.scala
--- a/src/Pure/Tools/doc.scala	Sat Apr 05 18:52:03 2014 +0200
+++ b/src/Pure/Tools/doc.scala	Sat Apr 05 19:07:05 2014 +0200
@@ -1,7 +1,7 @@
 /*  Title:      Pure/Tools/doc.scala
     Author:     Makarius
 
-View Isabelle documentation.
+Access to Isabelle documentation.
 */
 
 package isabelle
@@ -35,10 +35,10 @@
   case class Doc(name: String, title: String, path: Path) extends Entry
   case class Text_File(name: String, path: Path) extends Entry
 
-  def text_file(name: String): Option[Text_File] =
+  def text_file(name: Path): Option[Text_File] =
   {
-    val path = Path.variable("ISABELLE_HOME") + Path.explode(name)
-    if (path.is_file) Some(Text_File(name, path))
+    val path = Path.variable("ISABELLE_HOME") + name
+    if (path.is_file) Some(Text_File(name.implode, path))
     else None
   }
 
@@ -46,25 +46,16 @@
   private val Doc_Entry = new Regex("""^\s+(\S+)\s+(.+)\s*$""")
 
   private def release_notes(): List[Entry] =
-  {
-    val names =
-      List("ANNOUNCE", "README", "NEWS", "COPYRIGHT", "CONTRIBUTORS",
-        "contrib/README", "README_REPOSITORY")
     Section("Release notes", true) ::
-      (for (name <- names; entry <- text_file(name)) yield entry)
-  }
+      Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_RELEASE_NOTES")).flatMap(text_file(_))
 
   private def examples(): List[Entry] =
-  {
-    val names =
-      List(
-        "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")
-    Section("Examples", true) :: names.map(name => text_file(name).get)
-  }
+    Section("Examples", true) ::
+      Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_EXAMPLES")).map(file =>
+        text_file(file) match {
+          case Some(entry) => entry
+          case None => error("Bad ISABELLE_DOCS_EXAMPLES entry: " + file)
+        })
 
   def contents(): List[Entry] =
     (for {