# HG changeset patch
# User wenzelm
# Date 1379785726 -7200
# Node ID 06a6216f733ed338b8646695f14bb4c7b9bce6fd
# Parent  3806bf1d2a333e814896f63cb971ca7ba2bfa2d9
immediate access to some elementary examples;

diff -r 3806bf1d2a33 -r 06a6216f733e src/Pure/Tools/doc.scala
--- a/src/Pure/Tools/doc.scala	Sat Sep 21 17:37:02 2013 +0200
+++ b/src/Pure/Tools/doc.scala	Sat Sep 21 19:48:46 2013 +0200
@@ -35,17 +35,18 @@
   case class Doc(name: String, title: String) extends Entry
   case class Text_File(name: String, path: Path) extends Entry
 
+  def text_file(name: String): Option[Text_File] =
+  {
+    val path = Path.variable("ISABELLE_HOME") + Path.explode(name)
+    if (path.is_file) Some(Text_File(name, path))
+    else None
+  }
+
   private val Section_Entry = new Regex("""^(\S.*)\s*$""")
   private val Doc_Entry = new Regex("""^\s+(\S+)\s+(.+)\s*$""")
 
   private def release_notes(): List[Entry] =
   {
-    def text_file(name: String): Option[Text_File] =
-    {
-      val path = Path.variable("ISABELLE_HOME") + Path.explode(name)
-      if (path.is_file) Some(Text_File(name, path))
-      else None
-    }
     val names =
       List("ANNOUNCE", "README", "NEWS", "COPYRIGHT", "CONTRIBUTORS",
         "contrib/README", "README_REPOSITORY")
@@ -53,6 +54,16 @@
       (for (name <- names; entry <- text_file(name)) yield entry)
   }
 
+  private def examples(): List[Entry] =
+  {
+    val names =
+      List(
+        "src/HOL/ex/Seq.thy",
+        "src/HOL/Unix/Unix.thy",
+        "src/HOL/Isar_Examples/Drinker.thy")
+    Section("Examples") :: names.map(name => text_file(name).get)
+  }
+
   def contents(): List[Entry] =
     (for {
       line <- contents_lines()
@@ -62,7 +73,7 @@
           case Doc_Entry(name, title) => Some(Doc(name, title))
           case _ => None
         }
-    } yield entry) ::: release_notes()
+    } yield entry) ::: release_notes() ::: examples()
 
 
   /* view */